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