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	$$⊢\left(F:A⟶B\wedge ⟨C,D⟩\in F\right)\to \left(C\in A\wedge D\in B\right)$$

Proof

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