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