Theorem elmpocl

Description: If a two-parameter class is not empty, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015)

	Ref	Expression
Hypothesis	elmpocl.f	|- F = ( x e. A , y e. B |-> C )
Assertion	elmpocl	|- ( X e. ( S F T ) -> ( S e. A /\ T e. B ) )

Proof

Step	Hyp	Ref	Expression
1		elmpocl.f	|- F = ( x e. A , y e. B |-> C )
2		df-mpo	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
3	1 2	eqtri	|- F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
4	3	dmeqi	|- dom F = dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
5		dmoprabss	|- dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } C_ ( A X. B )
6	4 5	eqsstri	|- dom F C_ ( A X. B )
7		elfvdm	|- ( X e. ( F ` <. S , T >. ) -> <. S , T >. e. dom F )
8		df-ov	|- ( S F T ) = ( F ` <. S , T >. )
9	7 8	eleq2s	|- ( X e. ( S F T ) -> <. S , T >. e. dom F )
10	6 9	sselid	|- ( X e. ( S F T ) -> <. S , T >. e. ( A X. B ) )
11		opelxp	|- ( <. S , T >. e. ( A X. B ) <-> ( S e. A /\ T e. B ) )
12	10 11	sylib	|- ( X e. ( S F T ) -> ( S e. A /\ T e. B ) )