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

Metamath Proof Explorer

Theorem cbvopab2

Description: Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013)

Ref Expression
Hypotheses cbvopab2.1 
|- F/ z ph
cbvopab2.2 
|- F/ y ps
cbvopab2.3 
|- ( y = z -> ( ph <-> ps ) )
Assertion cbvopab2 
|- { <. x , y >. | ph } = { <. x , z >. | ps }

Proof

Step Hyp Ref Expression
1 cbvopab2.1 
 |-  F/ z ph
2 cbvopab2.2 
 |-  F/ y ps
3 cbvopab2.3 
 |-  ( y = z -> ( ph <-> ps ) )
4 nfv 
 |-  F/ z w = <. x , y >.
5 4 1 nfan 
 |-  F/ z ( w = <. x , y >. /\ ph )
6 nfv 
 |-  F/ y w = <. x , z >.
7 6 2 nfan 
 |-  F/ y ( w = <. x , z >. /\ ps )
8 opeq2 
 |-  ( y = z -> <. x , y >. = <. x , z >. )
9 8 eqeq2d 
 |-  ( y = z -> ( w = <. x , y >. <-> w = <. x , z >. ) )
10 9 3 anbi12d 
 |-  ( y = z -> ( ( w = <. x , y >. /\ ph ) <-> ( w = <. x , z >. /\ ps ) ) )
11 5 7 10 cbvexv1 
 |-  ( E. y ( w = <. x , y >. /\ ph ) <-> E. z ( w = <. x , z >. /\ ps ) )
12 11 exbii 
 |-  ( E. x E. y ( w = <. x , y >. /\ ph ) <-> E. x E. z ( w = <. x , z >. /\ ps ) )
13 12 abbii 
 |-  { w | E. x E. y ( w = <. x , y >. /\ ph ) } = { w | E. x E. z ( w = <. x , z >. /\ ps ) }
14 df-opab 
 |-  { <. x , y >. | ph } = { w | E. x E. y ( w = <. x , y >. /\ ph ) }
15 df-opab 
 |-  { <. x , z >. | ps } = { w | E. x E. z ( w = <. x , z >. /\ ps ) }
16 13 14 15 3eqtr4i 
 |-  { <. x , y >. | ph } = { <. x , z >. | ps }