Step |
Hyp |
Ref |
Expression |
1 |
|
biidd |
|- ( u = <. x , y >. -> ( z e. C <-> z e. C ) ) |
2 |
1
|
dfoprab4 |
|- { <. u , z >. | ( u e. ( A X. B ) /\ z e. C ) } = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z e. C ) } |
3 |
|
df-xp |
|- ( ( A X. B ) X. C ) = { <. u , z >. | ( u e. ( A X. B ) /\ z e. C ) } |
4 |
|
df-3an |
|- ( ( x e. A /\ y e. B /\ z e. C ) <-> ( ( x e. A /\ y e. B ) /\ z e. C ) ) |
5 |
4
|
oprabbii |
|- { <. <. x , y >. , z >. | ( x e. A /\ y e. B /\ z e. C ) } = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z e. C ) } |
6 |
2 3 5
|
3eqtr4i |
|- ( ( A X. B ) X. C ) = { <. <. x , y >. , z >. | ( x e. A /\ y e. B /\ z e. C ) } |