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) Avoid ax-10 , ax-12 . (Revised by SN, 7-Jun-2025)

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 elopab w z x y | φ x y w z = x y φ
4 excom x y w z = x y φ y x w z = x y φ
5 ancom w = x z = y z = y w = x
6 vex w V
7 vex z V
8 6 7 opth w z = x y w = x z = y
9 7 6 opth z w = y x z = y w = x
10 5 8 9 3bitr4i w z = x y z w = y x
11 10 anbi1i w z = x y φ z w = y x φ
12 11 2exbii y x w z = x y φ y x z w = y x φ
13 3 4 12 3bitri w z x y | φ y x z w = y x φ
14 7 6 opelcnv z w x y | φ -1 w z x y | φ
15 elopab z w y x | φ y x z w = y x φ
16 13 14 15 3bitr4i z w x y | φ -1 z w y x | φ
17 1 2 16 eqrelriiv x y | φ -1 = y x | φ