Step |
Hyp |
Ref |
Expression |
1 |
|
dmoprab |
|- dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } = { <. x , y >. | E. z ( ( x e. A /\ y e. B ) /\ ph ) } |
2 |
|
19.42v |
|- ( E. z ( ( x e. A /\ y e. B ) /\ ph ) <-> ( ( x e. A /\ y e. B ) /\ E. z ph ) ) |
3 |
2
|
opabbii |
|- { <. x , y >. | E. z ( ( x e. A /\ y e. B ) /\ ph ) } = { <. x , y >. | ( ( x e. A /\ y e. B ) /\ E. z ph ) } |
4 |
|
opabssxp |
|- { <. x , y >. | ( ( x e. A /\ y e. B ) /\ E. z ph ) } C_ ( A X. B ) |
5 |
3 4
|
eqsstri |
|- { <. x , y >. | E. z ( ( x e. A /\ y e. B ) /\ ph ) } C_ ( A X. B ) |
6 |
1 5
|
eqsstri |
|- dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } C_ ( A X. B ) |