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 e. dom F ) -> <. A , ( F ` A ) >. e. F )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( F ` A ) = ( F ` A )
2 funopfvb 
 |-  ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) = ( F ` A ) <-> <. A , ( F ` A ) >. e. F ) )
3 1 2 mpbii 
 |-  ( ( Fun F /\ A e. dom F ) -> <. A , ( F ` A ) >. e. F )