Theorem funopfv

Description: The second element in an ordered pair member of a function is the function's value. (Contributed by NM, 19-Jul-1996)

	Ref	Expression
Assertion	funopfv	⊢ ( Fun 𝐹 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 → ( 𝐹 ‘ 𝐴 ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-br	⊢ ( 𝐴 𝐹 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 )
2		funbrfv	⊢ ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 → ( 𝐹 ‘ 𝐴 ) = 𝐵 ) )
3	1 2	biimtrrid	⊢ ( Fun 𝐹 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 → ( 𝐹 ‘ 𝐴 ) = 𝐵 ) )