Theorem elmpocl

Description: If a two-parameter class is not empty, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015)

	Ref	Expression
Hypothesis	elmpocl.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion	elmpocl	⊢ ( 𝑋 ∈ ( 𝑆 𝐹 𝑇 ) → ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elmpocl.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2		df-mpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
3	1 2	eqtri	⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
4	3	dmeqi	⊢ dom 𝐹 = dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
5		dmoprabss	⊢ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } ⊆ ( 𝐴 × 𝐵 )
6	4 5	eqsstri	⊢ dom 𝐹 ⊆ ( 𝐴 × 𝐵 )
7		elfvdm	⊢ ( 𝑋 ∈ ( 𝐹 ‘ ⟨ 𝑆 , 𝑇 ⟩ ) → ⟨ 𝑆 , 𝑇 ⟩ ∈ dom 𝐹 )
8		df-ov	⊢ ( 𝑆 𝐹 𝑇 ) = ( 𝐹 ‘ ⟨ 𝑆 , 𝑇 ⟩ )
9	7 8	eleq2s	⊢ ( 𝑋 ∈ ( 𝑆 𝐹 𝑇 ) → ⟨ 𝑆 , 𝑇 ⟩ ∈ dom 𝐹 )
10	6 9	sselid	⊢ ( 𝑋 ∈ ( 𝑆 𝐹 𝑇 ) → ⟨ 𝑆 , 𝑇 ⟩ ∈ ( 𝐴 × 𝐵 ) )
11		opelxp	⊢ ( ⟨ 𝑆 , 𝑇 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐵 ) )
12	10 11	sylib	⊢ ( 𝑋 ∈ ( 𝑆 𝐹 𝑇 ) → ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐵 ) )