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 } |