Step |
Hyp |
Ref |
Expression |
1 |
|
eqeq1 |
|- ( z = w -> ( z = <. x , y >. <-> w = <. x , y >. ) ) |
2 |
1
|
anbi1d |
|- ( z = w -> ( ( z = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> ( w = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) ) |
3 |
2
|
2exbidv |
|- ( z = w -> ( E. x E. y ( z = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> E. x E. y ( w = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) ) |
4 |
|
eqeq1 |
|- ( w = A -> ( w = <. x , y >. <-> A = <. x , y >. ) ) |
5 |
4
|
anbi1d |
|- ( w = A -> ( ( w = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) ) |
6 |
5
|
2exbidv |
|- ( w = A -> ( E. x E. y ( w = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) ) |
7 |
|
df-xp |
|- ( B X. C ) = { <. x , y >. | ( x e. B /\ y e. C ) } |
8 |
|
df-opab |
|- { <. x , y >. | ( x e. B /\ y e. C ) } = { z | E. x E. y ( z = <. x , y >. /\ ( x e. B /\ y e. C ) ) } |
9 |
7 8
|
eqtri |
|- ( B X. C ) = { z | E. x E. y ( z = <. x , y >. /\ ( x e. B /\ y e. C ) ) } |
10 |
3 6 9
|
elab2gw |
|- ( A e. ( B X. C ) -> ( A e. ( B X. C ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) ) |
11 |
10
|
ibi |
|- ( A e. ( B X. C ) -> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) |