This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem csbcnv

Description: Move class substitution in and out of the converse of a relation. Version of csbcnvgALT without a sethood antecedent but depending on more axioms. (Contributed by Thierry Arnoux, 8-Feb-2017) (Revised by NM, 23-Aug-2018)

Ref Expression
Assertion csbcnv 
|- `' [_ A / x ]_ F = [_ A / x ]_ `' F

Proof

Step Hyp Ref Expression
1 sbcbr 
 |-  ( [. A / x ]. z F y <-> z [_ A / x ]_ F y )
2 1 opabbii 
 |-  { <. y , z >. | [. A / x ]. z F y } = { <. y , z >. | z [_ A / x ]_ F y }
3 csbopab 
 |-  [_ A / x ]_ { <. y , z >. | z F y } = { <. y , z >. | [. A / x ]. z F y }
4 df-cnv 
 |-  `' [_ A / x ]_ F = { <. y , z >. | z [_ A / x ]_ F y }
5 2 3 4 3eqtr4ri 
 |-  `' [_ A / x ]_ F = [_ A / x ]_ { <. y , z >. | z F y }
6 df-cnv 
 |-  `' F = { <. y , z >. | z F y }
7 6 csbeq2i 
 |-  [_ A / x ]_ `' F = [_ A / x ]_ { <. y , z >. | z F y }
8 5 7 eqtr4i 
 |-  `' [_ A / x ]_ F = [_ A / x ]_ `' F