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