Metamath Proof Explorer


Theorem fnopfv

Description: Ordered pair with function value. Part of Theorem 4.3(i) of Monk1 p. 41. (Contributed by NM, 30-Sep-2004)

Ref Expression
Assertion fnopfv FFnABABFBF

Proof

Step Hyp Ref Expression
1 funfvop FunFBdomFBFBF
2 1 funfni FFnABABFBF