Step |
Hyp |
Ref |
Expression |
1 |
|
cbvoprab12v.1 |
|- ( ( x = w /\ y = v ) -> ( ph <-> ps ) ) |
2 |
|
opeq12 |
|- ( ( x = w /\ y = v ) -> <. x , y >. = <. w , v >. ) |
3 |
2
|
opeq1d |
|- ( ( x = w /\ y = v ) -> <. <. x , y >. , z >. = <. <. w , v >. , z >. ) |
4 |
3
|
eqeq2d |
|- ( ( x = w /\ y = v ) -> ( u = <. <. x , y >. , z >. <-> u = <. <. w , v >. , z >. ) ) |
5 |
4 1
|
anbi12d |
|- ( ( x = w /\ y = v ) -> ( ( u = <. <. x , y >. , z >. /\ ph ) <-> ( u = <. <. w , v >. , z >. /\ ps ) ) ) |
6 |
5
|
exbidv |
|- ( ( x = w /\ y = v ) -> ( E. z ( u = <. <. x , y >. , z >. /\ ph ) <-> E. z ( u = <. <. w , v >. , z >. /\ ps ) ) ) |
7 |
6
|
cbvex2vw |
|- ( E. x E. y E. z ( u = <. <. x , y >. , z >. /\ ph ) <-> E. w E. v E. z ( u = <. <. w , v >. , z >. /\ ps ) ) |
8 |
7
|
abbii |
|- { u | E. x E. y E. z ( u = <. <. x , y >. , z >. /\ ph ) } = { u | E. w E. v E. z ( u = <. <. w , v >. , z >. /\ ps ) } |
9 |
|
df-oprab |
|- { <. <. x , y >. , z >. | ph } = { u | E. x E. y E. z ( u = <. <. x , y >. , z >. /\ ph ) } |
10 |
|
df-oprab |
|- { <. <. w , v >. , z >. | ps } = { u | E. w E. v E. z ( u = <. <. w , v >. , z >. /\ ps ) } |
11 |
8 9 10
|
3eqtr4i |
|- { <. <. x , y >. , z >. | ph } = { <. <. w , v >. , z >. | ps } |