This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
	Assertion	elmpocl1	⊢ ( 𝑋 ∈ ( 𝑆 𝐹 𝑇 ) → 𝑆 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elmpocl.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2	1	elmpocl	⊢ ( 𝑋 ∈ ( 𝑆 𝐹 𝑇 ) → ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐵 ) )
3	2	simpld	⊢ ( 𝑋 ∈ ( 𝑆 𝐹 𝑇 ) → 𝑆 ∈ 𝐴 )