Metamath Proof Explorer

Theorem fnop

Description: The first argument of an ordered pair in a function belongs to the function's domain. (Contributed by NM, 8-Aug-1994)

Ref Expression
Assertion fnop 
|- ( ( F Fn A /\ <. B , C >. e. F ) -> B e. A )

Proof

Step Hyp Ref Expression
1 df-br 
 |-  ( B F C <-> <. B , C >. e. F )
2 fnbr 
 |-  ( ( F Fn A /\ B F C ) -> B e. A )
3 1 2 sylan2br 
 |-  ( ( F Fn A /\ <. B , C >. e. F ) -> B e. A )