Metamath Proof Explorer


Theorem cnvopab

Description: The converse of a class abstraction of ordered pairs. (Contributed by NM, 11-Dec-2003) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion cnvopab x y | φ -1 = y x | φ

Proof

Step Hyp Ref Expression
1 relcnv Rel x y | φ -1
2 relopabv Rel y x | φ
3 vopelopabsb w z x y | φ w x z y φ
4 sbcom2 w x z y φ z y w x φ
5 3 4 bitri w z x y | φ z y w x φ
6 vex z V
7 vex w V
8 6 7 opelcnv z w x y | φ -1 w z x y | φ
9 vopelopabsb z w y x | φ z y w x φ
10 5 8 9 3bitr4i z w x y | φ -1 z w y x | φ
11 1 2 10 eqrelriiv x y | φ -1 = y x | φ