Theorem fnrel

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

	Ref	Expression
Assertion	fnrel	$$⊢FFnA\to \mathrm{Rel}F$$

Proof

Step	Hyp	Ref	Expression
1		fnfun	$$⊢FFnA\to \mathrm{Fun}F$$
2		funrel	$$⊢\mathrm{Fun}F\to \mathrm{Rel}F$$
3	1 2	syl	$$⊢FFnA\to \mathrm{Rel}F$$