Theorem funrel 4919

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

Assertion

Ref	Expression
funrel	⊢ (Fun 𝐴 → Rel 𝐴)

Proof of Theorem funrel

Step	Hyp	Ref	Expression
1		df-fun 4904	. 2 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ))
2	1	simplbi 259	1 ⊢ (Fun 𝐴 → Rel 𝐴)

Syntax hints:   → wi 4   ⊆ wss 2917   I cid 4025  ^◡ccnv 4344   ∘ ccom 4349  Rel wrel 4350  Fun wfun 4896

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99

This theorem depends on definitions:  df-bi 110  df-fun 4904

This theorem is referenced by:  funeu  4926  nfunv  4933  funopg  4934  funssres  4942  funun  4944  fununi  4967  funcnvres2  4974  funimaexg  4983  fnrel  4997  fcoi1  5070  f1orel  5129  funbrfv  5212  funbrfv2b  5218  fvmptss2  5247  funfvbrb  5280  fmptco  5330  elmpt2cl  5698  mpt2xopn0yelv  5854  tfrlem6  5932  fundmen  6286