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

Metamath Proof Explorer

Theorem csbcnvgALT

Description: Move class substitution in and out of the converse of a relation. Version of csbcnv with a sethood antecedent but depending on fewer axioms. (Contributed by Thierry Arnoux, 8-Feb-2017) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion csbcnvgALT 
|- ( A e. V -> `' [_ A / x ]_ F = [_ A / x ]_ `' F )

Proof

Step Hyp Ref Expression
1 sbcbr123 
 |-  ( [. A / x ]. z F y <-> [_ A / x ]_ z [_ A / x ]_ F [_ A / x ]_ y )
2 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ z = z )
3 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ y = y )
4 2 3 breq12d 
 |-  ( A e. V -> ( [_ A / x ]_ z [_ A / x ]_ F [_ A / x ]_ y <-> z [_ A / x ]_ F y ) )
5 1 4 bitrid 
 |-  ( A e. V -> ( [. A / x ]. z F y <-> z [_ A / x ]_ F y ) )
6 5 opabbidv 
 |-  ( A e. V -> { <. y , z >. | [. A / x ]. z F y } = { <. y , z >. | z [_ A / x ]_ F y } )
7 csbopabgALT 
 |-  ( A e. V -> [_ A / x ]_ { <. y , z >. | z F y } = { <. y , z >. | [. A / x ]. z F y } )
8 df-cnv 
 |-  `' [_ A / x ]_ F = { <. y , z >. | z [_ A / x ]_ F y }
9 8 a1i 
 |-  ( A e. V -> `' [_ A / x ]_ F = { <. y , z >. | z [_ A / x ]_ F y } )
10 6 7 9 3eqtr4rd 
 |-  ( A e. V -> `' [_ A / x ]_ F = [_ A / x ]_ { <. y , z >. | z F y } )
11 df-cnv 
 |-  `' F = { <. y , z >. | z F y }
12 11 csbeq2i 
 |-  [_ A / x ]_ `' F = [_ A / x ]_ { <. y , z >. | z F y }
13 10 12 eqtr4di 
 |-  ( A e. V -> `' [_ A / x ]_ F = [_ A / x ]_ `' F )