This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 >. | 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 }