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	$$⊢{\left\{⟨x,y⟩|\phi \right\}}^{-1}=\left\{⟨y,x⟩|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{\left\{⟨x,y⟩|\phi \right\}}^{-1}$$
2		relopabv	$$⊢\mathrm{Rel}\left\{⟨y,x⟩|\phi \right\}$$
3		elopab	$$⊢⟨w,z⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(⟨w,z⟩=⟨x,y⟩\wedge \phi \right)$$
4		excom	$$⊢\exists x\exists y\left(⟨w,z⟩=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists y\exists x\left(⟨w,z⟩=⟨x,y⟩\wedge \phi \right)$$
5		ancom	$$⊢\left(w=x\wedge z=y\right)\leftrightarrow \left(z=y\wedge w=x\right)$$
6		vex	$$⊢w\in \mathrm{V}$$
7		vex	$$⊢z\in \mathrm{V}$$
8	6 7	opth	$$⊢⟨w,z⟩=⟨x,y⟩\leftrightarrow \left(w=x\wedge z=y\right)$$
9	7 6	opth	$$⊢⟨z,w⟩=⟨y,x⟩\leftrightarrow \left(z=y\wedge w=x\right)$$
10	5 8 9	3bitr4i	$$⊢⟨w,z⟩=⟨x,y⟩\leftrightarrow ⟨z,w⟩=⟨y,x⟩$$
11	10	anbi1i	$$⊢\left(⟨w,z⟩=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(⟨z,w⟩=⟨y,x⟩\wedge \phi \right)$$
12	11	2exbii	$$⊢\exists y\exists x\left(⟨w,z⟩=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists y\exists x\left(⟨z,w⟩=⟨y,x⟩\wedge \phi \right)$$
13	3 4 12	3bitri	$$⊢⟨w,z⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists y\exists x\left(⟨z,w⟩=⟨y,x⟩\wedge \phi \right)$$
14	7 6	opelcnv	$$⊢⟨z,w⟩\in {\left\{⟨x,y⟩|\phi \right\}}^{-1}\leftrightarrow ⟨w,z⟩\in \left\{⟨x,y⟩|\phi \right\}$$
15		elopab	$$⊢⟨z,w⟩\in \left\{⟨y,x⟩|\phi \right\}\leftrightarrow \exists y\exists x\left(⟨z,w⟩=⟨y,x⟩\wedge \phi \right)$$
16	13 14 15	3bitr4i	$$⊢⟨z,w⟩\in {\left\{⟨x,y⟩|\phi \right\}}^{-1}\leftrightarrow ⟨z,w⟩\in \left\{⟨y,x⟩|\phi \right\}$$
17	1 2 16	eqrelriiv	$$⊢{\left\{⟨x,y⟩|\phi \right\}}^{-1}=\left\{⟨y,x⟩|\phi \right\}$$