Step |
Hyp |
Ref |
Expression |
1 |
|
cbvoprab3v.1 |
|- ( z = w -> ( ph <-> ps ) ) |
2 |
|
opeq2 |
|- ( z = w -> <. <. x , y >. , z >. = <. <. x , y >. , w >. ) |
3 |
2
|
eqeq2d |
|- ( z = w -> ( v = <. <. x , y >. , z >. <-> v = <. <. x , y >. , w >. ) ) |
4 |
3 1
|
anbi12d |
|- ( z = w -> ( ( v = <. <. x , y >. , z >. /\ ph ) <-> ( v = <. <. x , y >. , w >. /\ ps ) ) ) |
5 |
4
|
cbvexvw |
|- ( E. z ( v = <. <. x , y >. , z >. /\ ph ) <-> E. w ( v = <. <. x , y >. , w >. /\ ps ) ) |
6 |
5
|
2exbii |
|- ( E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) <-> E. x E. y E. w ( v = <. <. x , y >. , w >. /\ ps ) ) |
7 |
6
|
abbii |
|- { v | E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) } = { v | E. x E. y E. w ( v = <. <. x , y >. , w >. /\ ps ) } |
8 |
|
df-oprab |
|- { <. <. x , y >. , z >. | ph } = { v | E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) } |
9 |
|
df-oprab |
|- { <. <. x , y >. , w >. | ps } = { v | E. x E. y E. w ( v = <. <. x , y >. , w >. /\ ps ) } |
10 |
7 8 9
|
3eqtr4i |
|- { <. <. x , y >. , z >. | ph } = { <. <. x , y >. , w >. | ps } |