Step |
Hyp |
Ref |
Expression |
1 |
|
elxp |
|- ( A e. ( B X. C ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) |
2 |
|
eqcom |
|- ( <. x , y >. = A <-> A = <. x , y >. ) |
3 |
|
opelxp |
|- ( <. x , y >. e. ( B X. C ) <-> ( x e. B /\ y e. C ) ) |
4 |
2 3
|
anbi12i |
|- ( ( <. x , y >. = A /\ <. x , y >. e. ( B X. C ) ) <-> ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) |
5 |
4
|
2exbii |
|- ( E. x E. y ( <. x , y >. = A /\ <. x , y >. e. ( B X. C ) ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) |
6 |
1 5
|
bitr4i |
|- ( A e. ( B X. C ) <-> E. x E. y ( <. x , y >. = A /\ <. x , y >. e. ( B X. C ) ) ) |