Theorem funrel 5276

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

Syntax hints:   → wi 4   ⊆ wss 3157   I cid 4324  ^◡ccnv 4663   ∘ ccom 4668  Rel wrel 4669  Fun wfun 5253

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

This theorem depends on definitions:  df-bi 117  df-fun 5261

This theorem is referenced by:  0nelfun  5277  funeu  5284  nfunv  5292  funopg  5293  funssres  5301  funun  5303  fununi  5327  funcnvres2  5334  funimaexg  5343  fnrel  5357  fcoi1  5441  f1orel  5510  funbrfv  5602  funbrfv2b  5608  fvmptss2  5639  mptrcl  5647  elfvmptrab1  5659  funfvbrb  5678  fmptco  5731  funresdfunsnss  5768  elmpocl  6122  funexw  6178  mpoxopn0yelv  6306  tfrlem6  6383  funresdfunsndc  6573  pmresg  6744  fundmen  6874  caseinl  7166  caseinr  7167  axaddf  7952  axmulf  7953  hashinfom  10887  4sqlemffi  12590  structcnvcnv  12719  lidlmex  14107  istopon  14333  eltg4i  14375  eltg3  14377  tg1  14379  tg2  14380  tgclb  14385  lmrcl  14511