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

Metamath Proof Explorer

Theorem cbvopab1

Description: Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 6-Oct-2004) (Revised by Mario Carneiro, 14-Oct-2016) Add disjoint variable condition to avoid ax-13 . See cbvopab1g for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 cbvopab1.1 
 |-  F/ z ph
2 cbvopab1.2 
 |-  F/ x ps
3 cbvopab1.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 nfsbv 
 |-  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 2 3 sbhypf 
 |-  ( v = z -> ( [ v / x ] ph <-> ps ) )
23 21 22 anbi12d 
 |-  ( v = z -> ( ( w = <. v , y >. /\ [ v / x ] ph ) <-> ( w = <. z , y >. /\ ps ) ) )
24 23 exbidv 
 |-  ( v = z -> ( E. y ( w = <. v , y >. /\ [ v / x ] ph ) <-> E. y ( w = <. z , y >. /\ ps ) ) )
25 18 19 24 cbvexv1 
 |-  ( E. v E. y ( w = <. v , y >. /\ [ v / x ] ph ) <-> E. z E. y ( w = <. z , y >. /\ ps ) )
26 14 25 bitri 
 |-  ( E. x E. y ( w = <. x , y >. /\ ph ) <-> E. z E. y ( w = <. z , y >. /\ ps ) )
27 26 abbii 
 |-  { w | E. x E. y ( w = <. x , y >. /\ ph ) } = { w | E. z E. y ( w = <. z , y >. /\ ps ) }
28 df-opab 
 |-  { <. x , y >. | ph } = { w | E. x E. y ( w = <. x , y >. /\ ph ) }
29 df-opab 
 |-  { <. z , y >. | ps } = { w | E. z E. y ( w = <. z , y >. /\ ps ) }
30 27 28 29 3eqtr4i 
 |-  { <. x , y >. | ph } = { <. z , y >. | ps }