Theorem funrel 5032

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 5017	. 2 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ))
2	1	simplbi 268	1 ⊢ (Fun 𝐴 → Rel 𝐴)

Syntax hints:   → wi 4   ⊆ wss 2999   I cid 4115  ^◡ccnv 4437   ∘ ccom 4442  Rel wrel 4443  Fun wfun 5009

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

This theorem depends on definitions:  df-bi 115  df-fun 5017

This theorem is referenced by:  0nelfun  5033  funeu  5040  nfunv  5047  funopg  5048  funssres  5056  funun  5058  fununi  5082  funcnvres2  5089  funimaexg  5098  fnrel  5112  fcoi1  5191  f1orel  5256  funbrfv  5343  funbrfv2b  5349  fvmptss2  5379  funfvbrb  5412  fmptco  5464  funresdfunsnss  5500  elmpt2cl  5842  mpt2xopn0yelv  6004  tfrlem6  6081  funresdfunsndc  6265  pmresg  6433  fundmen  6523  hashinfom  10186  structcnvcnv  11510  istopon  11610