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 V A / x F -1 = A / x F -1

Proof

Step Hyp Ref Expression
1 sbcbr123 [˙A / x]˙ z F y A / x z A / x F A / x y
2 csbconstg A V A / x z = z
3 csbconstg A V A / x y = y
4 2 3 breq12d A V A / x z A / x F A / x y z A / x F y
5 1 4 syl5bb A V [˙A / x]˙ z F y z A / x F y
6 5 opabbidv A V y z | [˙A / x]˙ z F y = y z | z A / x F y
7 csbopabgALT A V A / x y z | z F y = y z | [˙A / x]˙ z F y
8 df-cnv A / x F -1 = y z | z A / x F y
9 8 a1i A V A / x F -1 = y z | z A / x F y
10 6 7 9 3eqtr4rd A V A / x F -1 = A / x y z | z F y
11 df-cnv F -1 = y z | z F y
12 11 csbeq2i A / x F -1 = A / x y z | z F y
13 10 12 eqtr4di A V A / x F -1 = A / x F -1