Theorem funrel 5338

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

Syntax hints:   → wi 4   ⊆ wss 3197   I cid 4380  ^◡ccnv 4719   ∘ ccom 4724  Rel wrel 4725  Fun wfun 5315

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 5323

This theorem is referenced by:  0nelfun  5339  funeu  5346  nfunv  5354  funopg  5355  funssres  5363  funun  5365  fununfun  5367  fununi  5392  funcnvres2  5399  funimaexg  5408  fnrel  5422  fcoi1  5511  f1orel  5580  funbrfv  5675  funbrfv2b  5683  fvmptss2  5714  mptrcl  5722  elfvmptrab1  5734  funfvbrb  5753  fmptco  5806  funopsn  5822  funresdfunsnss  5849  elmpocl  6209  relmptopab  6216  funexw  6266  mpoxopn0yelv  6396  tfrlem6  6473  funresdfunsndc  6665  pmresg  6836  fundmen  6972  caseinl  7274  caseinr  7275  axaddf  8071  axmulf  8072  hashinfom  11017  4sqlemffi  12940  structcnvcnv  13069  lidlmex  14460  istopon  14708  eltg4i  14750  eltg3  14752  tg1  14754  tg2  14755  tgclb  14760  lmrcl  14887  1vgrex  15842  edg0iedg0g  15887  umgrnloopv  15935  edg0usgr  16066