Metamath Proof Explorer


Theorem funfvop

Description: Ordered pair with function value. Part of Theorem 4.3(i) of Monk1 p. 41. (Contributed by NM, 14-Oct-1996)

Ref Expression
Assertion funfvop FunFAdomFAFAF

Proof

Step Hyp Ref Expression
1 eqid FA=FA
2 funopfvb FunFAdomFFA=FAAFAF
3 1 2 mpbii FunFAdomFAFAF