Step |
Hyp |
Ref |
Expression |
1 |
|
cbvoprab3.1 |
|- F/ w ph |
2 |
|
cbvoprab3.2 |
|- F/ z ps |
3 |
|
cbvoprab3.3 |
|- ( z = w -> ( ph <-> ps ) ) |
4 |
|
nfv |
|- F/ w v = <. x , y >. |
5 |
4 1
|
nfan |
|- F/ w ( v = <. x , y >. /\ ph ) |
6 |
5
|
nfex |
|- F/ w E. y ( v = <. x , y >. /\ ph ) |
7 |
6
|
nfex |
|- F/ w E. x E. y ( v = <. x , y >. /\ ph ) |
8 |
|
nfv |
|- F/ z v = <. x , y >. |
9 |
8 2
|
nfan |
|- F/ z ( v = <. x , y >. /\ ps ) |
10 |
9
|
nfex |
|- F/ z E. y ( v = <. x , y >. /\ ps ) |
11 |
10
|
nfex |
|- F/ z E. x E. y ( v = <. x , y >. /\ ps ) |
12 |
3
|
anbi2d |
|- ( z = w -> ( ( v = <. x , y >. /\ ph ) <-> ( v = <. x , y >. /\ ps ) ) ) |
13 |
12
|
2exbidv |
|- ( z = w -> ( E. x E. y ( v = <. x , y >. /\ ph ) <-> E. x E. y ( v = <. x , y >. /\ ps ) ) ) |
14 |
7 11 13
|
cbvopab2 |
|- { <. v , z >. | E. x E. y ( v = <. x , y >. /\ ph ) } = { <. v , w >. | E. x E. y ( v = <. x , y >. /\ ps ) } |
15 |
|
dfoprab2 |
|- { <. <. x , y >. , z >. | ph } = { <. v , z >. | E. x E. y ( v = <. x , y >. /\ ph ) } |
16 |
|
dfoprab2 |
|- { <. <. x , y >. , w >. | ps } = { <. v , w >. | E. x E. y ( v = <. x , y >. /\ ps ) } |
17 |
14 15 16
|
3eqtr4i |
|- { <. <. x , y >. , z >. | ph } = { <. <. x , y >. , w >. | ps } |