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 Fun F A dom F A F A F


Step Hyp Ref Expression
1 eqid F A = F A
2 funopfvb Fun F A dom F F A = F A A F A F
3 1 2 mpbii Fun F A dom F A F A F