Metamath Proof Explorer

Theorem funopfv

Description: The second element in an ordered pair member of a function is the function's value. (Contributed by NM, 19-Jul-1996)

Ref Expression
Assertion funopfv 
|- ( Fun F -> ( <. A , B >. e. F -> ( F ` A ) = B ) )

Proof

Step Hyp Ref Expression
1 df-br 
 |-  ( A F B <-> <. A , B >. e. F )
2 funbrfv 
 |-  ( Fun F -> ( A F B -> ( F ` A ) = B ) )
3 1 2 syl5bir 
 |-  ( Fun F -> ( <. A , B >. e. F -> ( F ` A ) = B ) )