This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funopfvb

Description: Equivalence of function value and ordered pair membership. Theorem 4.3(ii) of Monk1 p. 42. (Contributed by NM, 26-Jan-1997)

Ref Expression
Assertion funopfvb ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A = B ↔ A B ∈ F

Proof

Step Hyp Ref Expression
1 funfn ⊢ Fun ⁡ F ↔ F Fn dom ⁡ F
2 fnopfvb ⊢ F Fn dom ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A = B ↔ A B ∈ F
3 1 2 sylanb ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A = B ↔ A B ∈ F