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 
|- ( ( F Fn A /\ B e. A ) -> <. B , ( F ` B ) >. e. F )

Proof

Step Hyp Ref Expression
1 funfvop 
 |-  ( ( Fun F /\ B e. dom F ) -> <. B , ( F ` B ) >. e. F )
2 1 funfni 
 |-  ( ( F Fn A /\ B e. A ) -> <. B , ( F ` B ) >. e. F )