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 )