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 >. | ph } = { <. y , x >. | ph }

Proof

Step	Hyp	Ref	Expression
1		relcnv	|- Rel `' { <. x , y >. | ph }
2		relopabv	|- Rel { <. y , x >. | ph }
3		elopab	|- ( <. w , z >. e. { <. x , y >. | ph } <-> E. x E. y ( <. w , z >. = <. x , y >. /\ ph ) )
4		excom	|- ( E. x E. y ( <. w , z >. = <. x , y >. /\ ph ) <-> E. y E. x ( <. w , z >. = <. x , y >. /\ ph ) )
5		ancom	|- ( ( w = x /\ z = y ) <-> ( z = y /\ w = x ) )
6		vex	|- w e. _V
7		vex	|- z e. _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 >. /\ ph ) <-> ( <. z , w >. = <. y , x >. /\ ph ) )
12	11	2exbii	|- ( E. y E. x ( <. w , z >. = <. x , y >. /\ ph ) <-> E. y E. x ( <. z , w >. = <. y , x >. /\ ph ) )
13	3 4 12	3bitri	|- ( <. w , z >. e. { <. x , y >. | ph } <-> E. y E. x ( <. z , w >. = <. y , x >. /\ ph ) )
14	7 6	opelcnv	|- ( <. z , w >. e. `' { <. x , y >. | ph } <-> <. w , z >. e. { <. x , y >. | ph } )
15		elopab	|- ( <. z , w >. e. { <. y , x >. | ph } <-> E. y E. x ( <. z , w >. = <. y , x >. /\ ph ) )
16	13 14 15	3bitr4i	|- ( <. z , w >. e. `' { <. x , y >. | ph } <-> <. z , w >. e. { <. y , x >. | ph } )
17	1 2 16	eqrelriiv	|- `' { <. x , y >. | ph } = { <. y , x >. | ph }