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=\left(x\in A,y\in B⟼C\right)$$
Assertion	elmpocl1	$$⊢X\in \left(SFT\right)\to S\in A$$

Proof

Step	Hyp	Ref	Expression
1		elmpocl.f	$$⊢F=\left(x\in A,y\in B⟼C\right)$$
2	1	elmpocl	$$⊢X\in \left(SFT\right)\to \left(S\in A\wedge T\in B\right)$$
3	2	simpld	$$⊢X\in \left(SFT\right)\to S\in A$$