Theorem funrel

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

	Ref	Expression
Assertion	funrel	$$⊢\mathrm{Fun}A\to \mathrm{Rel}A$$

Proof

Step	Hyp	Ref	Expression
1		df-fun	$$⊢\mathrm{Fun}A\leftrightarrow \left(\mathrm{Rel}A\wedge A\circ A^{-1}\subseteq \mathrm{I}\right)$$
2	1	simplbi	$$⊢\mathrm{Fun}A\to \mathrm{Rel}A$$