Metamath Proof Explorer


Theorem dmopabss

Description: Upper bound for the domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004)

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

Proof

Step Hyp Ref Expression
1 dmopab
 |-  dom { <. x , y >. | ( x e. A /\ ph ) } = { x | E. y ( x e. A /\ ph ) }
2 19.42v
 |-  ( E. y ( x e. A /\ ph ) <-> ( x e. A /\ E. y ph ) )
3 2 abbii
 |-  { x | E. y ( x e. A /\ ph ) } = { x | ( x e. A /\ E. y ph ) }
4 ssab2
 |-  { x | ( x e. A /\ E. y ph ) } C_ A
5 3 4 eqsstri
 |-  { x | E. y ( x e. A /\ ph ) } C_ A
6 1 5 eqsstri
 |-  dom { <. x , y >. | ( x e. A /\ ph ) } C_ A