Step |
Hyp |
Ref |
Expression |
1 |
|
n0 |
|- ( { <. x , y >. | ph } =/= (/) <-> E. z z e. { <. x , y >. | ph } ) |
2 |
|
elopab |
|- ( z e. { <. x , y >. | ph } <-> E. x E. y ( z = <. x , y >. /\ ph ) ) |
3 |
2
|
exbii |
|- ( E. z z e. { <. x , y >. | ph } <-> E. z E. x E. y ( z = <. x , y >. /\ ph ) ) |
4 |
|
exrot3 |
|- ( E. z E. x E. y ( z = <. x , y >. /\ ph ) <-> E. x E. y E. z ( z = <. x , y >. /\ ph ) ) |
5 |
|
opex |
|- <. x , y >. e. _V |
6 |
5
|
isseti |
|- E. z z = <. x , y >. |
7 |
|
19.41v |
|- ( E. z ( z = <. x , y >. /\ ph ) <-> ( E. z z = <. x , y >. /\ ph ) ) |
8 |
6 7
|
mpbiran |
|- ( E. z ( z = <. x , y >. /\ ph ) <-> ph ) |
9 |
8
|
2exbii |
|- ( E. x E. y E. z ( z = <. x , y >. /\ ph ) <-> E. x E. y ph ) |
10 |
4 9
|
bitri |
|- ( E. z E. x E. y ( z = <. x , y >. /\ ph ) <-> E. x E. y ph ) |
11 |
3 10
|
bitri |
|- ( E. z z e. { <. x , y >. | ph } <-> E. x E. y ph ) |
12 |
1 11
|
bitri |
|- ( { <. x , y >. | ph } =/= (/) <-> E. x E. y ph ) |