Theorem elmpocl1

Description: If a two-parameter class is not empty, the first argument is in its nominal domain. (Contributed by FL, 15-Oct-2012) (Revised by Stefan O'Rear, 7-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		elmpocl.f	|- F = ( x e. A , y e. B |-> C )
2	1	elmpocl	|- ( X e. ( S F T ) -> ( S e. A /\ T e. B ) )
3	2	simpld	|- ( X e. ( S F T ) -> S e. A )