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

Metamath Proof Explorer

Theorem cnvopabOLD

Description: Obsolete version of cnvopab as of 7-Jun-2025. (Contributed by NM, 11-Dec-2003) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cnvopabOLD 
|- `' { <. 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 }