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 |
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 |