Theorem elmpocl2

Description: If a two-parameter class is not empty, the second 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	elmpocl2	|- ( X e. ( S F T ) -> T e. B )

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	simprd	|- ( X e. ( S F T ) -> T e. B )