Theorem fnop

Description: The first argument of an ordered pair in a function belongs to the function's domain. (Contributed by NM, 8-Aug-1994)

	Ref	Expression
Assertion	fnop	⊢ ( ( 𝐹 Fn 𝐴 ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐹 ) → 𝐵 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-br	⊢ ( 𝐵 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐹 )
2		fnbr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 𝐹 𝐶 ) → 𝐵 ∈ 𝐴 )
3	1 2	sylan2br	⊢ ( ( 𝐹 Fn 𝐴 ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐹 ) → 𝐵 ∈ 𝐴 )