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

Proof

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