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)

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 vopelopabsb
 |-  ( <. w , z >. e. { <. x , y >. | ph } <-> [ w / x ] [ z / y ] ph )
4 sbcom2
 |-  ( [ w / x ] [ z / y ] ph <-> [ z / y ] [ w / x ] ph )
5 3 4 bitri
 |-  ( <. w , z >. e. { <. x , y >. | ph } <-> [ z / y ] [ w / x ] ph )
6 vex
 |-  z e. _V
7 vex
 |-  w e. _V
8 6 7 opelcnv
 |-  ( <. z , w >. e. `' { <. x , y >. | ph } <-> <. w , z >. e. { <. x , y >. | ph } )
9 vopelopabsb
 |-  ( <. z , w >. e. { <. y , x >. | ph } <-> [ z / y ] [ w / x ] ph )
10 5 8 9 3bitr4i
 |-  ( <. z , w >. e. `' { <. x , y >. | ph } <-> <. z , w >. e. { <. y , x >. | ph } )
11 1 2 10 eqrelriiv
 |-  `' { <. x , y >. | ph } = { <. y , x >. | ph }