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  7954  axmulf  7955  hashinfom  10889  4sqlemffi  12592  structcnvcnv  12721  lidlmex  14109  istopon  14335  eltg4i  14377  eltg3  14379  tg1  14381  tg2  14382  tgclb  14387  lmrcl  14513