This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )