Metamath Proof Explorer


Theorem fnopfvb

Description: Equivalence of function value and ordered pair membership. (Contributed by NM, 7-Nov-1995)

Ref Expression
Assertion fnopfvb ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ( 𝐹𝐵 ) = 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 fnbrfvb ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ( 𝐹𝐵 ) = 𝐶𝐵 𝐹 𝐶 ) )
2 df-br ( 𝐵 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐹 )
3 1 2 bitrdi ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ( 𝐹𝐵 ) = 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐹 ) )