Metamath Proof Explorer

Theorem fnopfvb

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

Ref Expression
Assertion fnopfvb ⊢ F Fn A ∧ B ∈ A → F ⁡ B = C ↔ B C ∈ F

Proof

Step Hyp Ref Expression
1 fnbrfvb ⊢ F Fn A ∧ B ∈ A → F ⁡ B = C ↔ B F C
2 df-br ⊢ B F C ↔ B C ∈ F
3 1 2 bitrdi ⊢ F Fn A ∧ B ∈ A → F ⁡ B = C ↔ B C ∈ F