Metamath Proof Explorer

Theorem cbvopab1g

Description: Change first bound variable in an ordered-pair class abstraction, using explicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . See cbvopab1 for a version with more disjoint variable conditions, but not requiring ax-13 . (Contributed by NM, 6-Oct-2004) (Revised by Mario Carneiro, 14-Oct-2016) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cbvopab1g.1 
 |-  F/ z ph
2 cbvopab1g.2 
 |-  F/ x ps
3 cbvopab1g.3 
 |-  ( x = z -> ( ph <-> ps ) )
4 nfv 
 |-  F/ v E. y ( w = <. x , y >. /\ ph )
5 nfv 
 |-  F/ x w = <. v , y >.
6 nfs1v 
 |-  F/ x [ v / x ] ph
7 5 6 nfan 
 |-  F/ x ( w = <. v , y >. /\ [ v / x ] ph )
8 7 nfex 
 |-  F/ x E. y ( w = <. v , y >. /\ [ v / x ] ph )
9 opeq1 
 |-  ( x = v -> <. x , y >. = <. v , y >. )
10 9 eqeq2d 
 |-  ( x = v -> ( w = <. x , y >. <-> w = <. v , y >. ) )
11 sbequ12 
 |-  ( x = v -> ( ph <-> [ v / x ] ph ) )
12 10 11 anbi12d 
 |-  ( x = v -> ( ( w = <. x , y >. /\ ph ) <-> ( w = <. v , y >. /\ [ v / x ] ph ) ) )
13 12 exbidv 
 |-  ( x = v -> ( E. y ( w = <. x , y >. /\ ph ) <-> E. y ( w = <. v , y >. /\ [ v / x ] ph ) ) )
14 4 8 13 cbvexv1 
 |-  ( E. x E. y ( w = <. x , y >. /\ ph ) <-> E. v E. y ( w = <. v , y >. /\ [ v / x ] ph ) )
15 nfv 
 |-  F/ z w = <. v , y >.
16 1 nfsb 
 |-  F/ z [ v / x ] ph
17 15 16 nfan 
 |-  F/ z ( w = <. v , y >. /\ [ v / x ] ph )
18 17 nfex 
 |-  F/ z E. y ( w = <. v , y >. /\ [ v / x ] ph )
19 nfv 
 |-  F/ v E. y ( w = <. z , y >. /\ ps )
20 opeq1 
 |-  ( v = z -> <. v , y >. = <. z , y >. )
21 20 eqeq2d 
 |-  ( v = z -> ( w = <. v , y >. <-> w = <. z , y >. ) )
22 sbequ 
 |-  ( v = z -> ( [ v / x ] ph <-> [ z / x ] ph ) )
23 2 3 sbie 
 |-  ( [ z / x ] ph <-> ps )
24 22 23 bitrdi 
 |-  ( v = z -> ( [ v / x ] ph <-> ps ) )
25 21 24 anbi12d 
 |-  ( v = z -> ( ( w = <. v , y >. /\ [ v / x ] ph ) <-> ( w = <. z , y >. /\ ps ) ) )
26 25 exbidv 
 |-  ( v = z -> ( E. y ( w = <. v , y >. /\ [ v / x ] ph ) <-> E. y ( w = <. z , y >. /\ ps ) ) )
27 18 19 26 cbvexv1 
 |-  ( E. v E. y ( w = <. v , y >. /\ [ v / x ] ph ) <-> E. z E. y ( w = <. z , y >. /\ ps ) )
28 14 27 bitri 
 |-  ( E. x E. y ( w = <. x , y >. /\ ph ) <-> E. z E. y ( w = <. z , y >. /\ ps ) )
29 28 abbii 
 |-  { w | E. x E. y ( w = <. x , y >. /\ ph ) } = { w | E. z E. y ( w = <. z , y >. /\ ps ) }
30 df-opab 
 |-  { <. x , y >. | ph } = { w | E. x E. y ( w = <. x , y >. /\ ph ) }
31 df-opab 
 |-  { <. z , y >. | ps } = { w | E. z E. y ( w = <. z , y >. /\ ps ) }
32 29 30 31 3eqtr4i 
 |-  { <. x , y >. | ph } = { <. z , y >. | ps }