Theorem funrel 5205

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

Syntax hints:   → wi 4   ⊆ wss 3116   I cid 4266  ^◡ccnv 4603   ∘ ccom 4608  Rel wrel 4609  Fun wfun 5182

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

This theorem depends on definitions:  df-bi 116  df-fun 5190

This theorem is referenced by:  0nelfun  5206  funeu  5213  nfunv  5221  funopg  5222  funssres  5230  funun  5232  fununi  5256  funcnvres2  5263  funimaexg  5272  fnrel  5286  fcoi1  5368  f1orel  5435  funbrfv  5525  funbrfv2b  5531  fvmptss2  5561  mptrcl  5568  elfvmptrab1  5580  funfvbrb  5598  fmptco  5651  funresdfunsnss  5688  elmpocl  6036  funexw  6080  mpoxopn0yelv  6207  tfrlem6  6284  funresdfunsndc  6474  pmresg  6642  fundmen  6772  caseinl  7056  caseinr  7057  axaddf  7809  axmulf  7810  hashinfom  10691  structcnvcnv  12410  istopon  12651  eltg4i  12695  eltg3  12697  tg1  12699  tg2  12700  tgclb  12705  lmrcl  12831