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	$$⊢{\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		relopab	$$⊢\mathrm{Rel}\left\{⟨y,x⟩|\phi \right\}$$
3		opelopabsbALT	$$⊢⟨w,z⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \left[z/y\right]\left[w/x\right]\phi$$
4		sbcom2	$$⊢\left[z/y\right]\left[w/x\right]\phi \leftrightarrow \left[w/x\right]\left[z/y\right]\phi$$
5	3 4	bitri	$$⊢⟨w,z⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \left[w/x\right]\left[z/y\right]\phi$$
6		vex	$$⊢z\in \mathrm{V}$$
7		vex	$$⊢w\in \mathrm{V}$$
8	6 7	opelcnv	$$⊢⟨z,w⟩\in {\left\{⟨x,y⟩|\phi \right\}}^{-1}\leftrightarrow ⟨w,z⟩\in \left\{⟨x,y⟩|\phi \right\}$$
9		opelopabsbALT	$$⊢⟨z,w⟩\in \left\{⟨y,x⟩|\phi \right\}\leftrightarrow \left[w/x\right]\left[z/y\right]\phi$$
10	5 8 9	3bitr4i	$$⊢⟨z,w⟩\in {\left\{⟨x,y⟩|\phi \right\}}^{-1}\leftrightarrow ⟨z,w⟩\in \left\{⟨y,x⟩|\phi \right\}$$
11	1 2 10	eqrelriiv	$$⊢{\left\{⟨x,y⟩|\phi \right\}}^{-1}=\left\{⟨y,x⟩|\phi \right\}$$