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

Metamath Proof Explorer

Theorem opelf

Description: The members of an ordered pair element of a mapping belong to the mapping's domain and codomain. (Contributed by NM, 10-Dec-2003) (Revised by Mario Carneiro, 26-Apr-2015)

		Ref	Expression
	Assertion	opelf	$⊢ (F : A ⟶ B \land ⟨C, D⟩ \in F) \to (C \in A \land D \in B)$

Proof

Step	Hyp	Ref	Expression
1		fssxp	$⊢ F : A ⟶ B \to F \subseteq A \times B$
2	1	sseld	$⊢ F : A ⟶ B \to (⟨C, D⟩ \in F \to ⟨C, D⟩ \in (A \times B))$
3		opelxp	$⊢ ⟨C, D⟩ \in (A \times B) \leftrightarrow (C \in A \land D \in B)$
4	2 3	imbitrdi	$⊢ F : A ⟶ B \to (⟨C, D⟩ \in F \to (C \in A \land D \in B))$
5	4	imp	$⊢ (F : A ⟶ B \land ⟨C, D⟩ \in F) \to (C \in A \land D \in B)$