Metamath Proof Explorer

Theorem fnrel

Description: A function with domain is a relation. (Contributed by NM, 1-Aug-1994)

Ref Expression
Assertion fnrel 
|- ( F Fn A -> Rel F )

Proof

Step Hyp Ref Expression
1 fnfun 
 |-  ( F Fn A -> Fun F )
2 funrel 
 |-  ( Fun F -> Rel F )
3 1 2 syl 
 |-  ( F Fn A -> Rel F )