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 xy|φ-1=yx|φ

Proof

Step Hyp Ref Expression
1 relcnv Relxy|φ-1
2 relopabv Relyx|φ
3 elopab wzxy|φxywz=xyφ
4 excom xywz=xyφyxwz=xyφ
5 ancom w=xz=yz=yw=x
6 vex wV
7 vex zV
8 6 7 opth wz=xyw=xz=y
9 7 6 opth zw=yxz=yw=x
10 5 8 9 3bitr4i wz=xyzw=yx
11 10 anbi1i wz=xyφzw=yxφ
12 11 2exbii yxwz=xyφyxzw=yxφ
13 3 4 12 3bitri wzxy|φyxzw=yxφ
14 7 6 opelcnv zwxy|φ-1wzxy|φ
15 elopab zwyx|φyxzw=yxφ
16 13 14 15 3bitr4i zwxy|φ-1zwyx|φ
17 1 2 16 eqrelriiv xy|φ-1=yx|φ