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	$⊢ F = (x \in A, y \in B ⟼ C)$
	Assertion	elmpocl	$⊢ X \in (S F T) \to (S \in A \land T \in B)$

Step	Hyp	Ref	Expression
1		elmpocl.f	$⊢ F = (x \in A, y \in B ⟼ C)$
2		df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
3	1 2	eqtri	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
4	3	dmeqi	$⊢ dom F = dom \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
5		dmoprabss	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\} \subseteq A \times B$
6	4 5	eqsstri	$⊢ dom F \subseteq A \times B$
7		elfvdm	$⊢ X \in F (⟨S, T⟩) \to ⟨S, T⟩ \in dom F$
8		df-ov	$⊢ S F T = F (⟨S, T⟩)$
9	7 8	eleq2s	$⊢ X \in (S F T) \to ⟨S, T⟩ \in dom F$
10	6 9	sseldi	$⊢ X \in (S F T) \to ⟨S, T⟩ \in (A \times B)$
11		opelxp	$⊢ ⟨S, T⟩ \in (A \times B) \leftrightarrow (S \in A \land T \in B)$
12	10 11	sylib	$⊢ X \in (S F T) \to (S \in A \land T \in B)$

Metamath Proof Explorer