Step |
Hyp |
Ref |
Expression |
1 |
|
copsex2g.1 |
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) |
2 |
|
eqcom |
|- ( <. A , B >. = <. x , y >. <-> <. x , y >. = <. A , B >. ) |
3 |
|
vex |
|- x e. _V |
4 |
|
vex |
|- y e. _V |
5 |
3 4
|
opth |
|- ( <. x , y >. = <. A , B >. <-> ( x = A /\ y = B ) ) |
6 |
2 5
|
bitri |
|- ( <. A , B >. = <. x , y >. <-> ( x = A /\ y = B ) ) |
7 |
6
|
anbi1i |
|- ( ( <. A , B >. = <. x , y >. /\ ph ) <-> ( ( x = A /\ y = B ) /\ ph ) ) |
8 |
7
|
2exbii |
|- ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> E. x E. y ( ( x = A /\ y = B ) /\ ph ) ) |
9 |
|
id |
|- ( ( x = A /\ y = B ) -> ( x = A /\ y = B ) ) |
10 |
9 1
|
cgsex2g |
|- ( ( A e. V /\ B e. W ) -> ( E. x E. y ( ( x = A /\ y = B ) /\ ph ) <-> ps ) ) |
11 |
8 10
|
syl5bb |
|- ( ( A e. V /\ B e. W ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) ) |