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