Metamath Proof Explorer


Theorem dmoprabss

Description: The domain of an operation class abstraction. (Contributed by NM, 24-Aug-1995)

Ref Expression
Assertion dmoprabss
|- dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } C_ ( A X. B )

Proof

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 )