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	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝐹 ) → ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fssxp	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 ⊆ ( 𝐴 × 𝐵 ) )
2	1	sseld	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝐹 → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
3		opelxp	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) )
4	2 3	imbitrdi	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝐹 → ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) )
5	4	imp	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝐹 ) → ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) )