Theorem funrel 5311

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

Syntax hints:   → wi 4   ⊆ wss 3177   I cid 4356  ^◡ccnv 4695   ∘ ccom 4700  Rel wrel 4701  Fun wfun 5288

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 5296

This theorem is referenced by:  0nelfun  5312  funeu  5319  nfunv  5327  funopg  5328  funssres  5336  funun  5338  fununfun  5340  fununi  5365  funcnvres2  5372  funimaexg  5381  fnrel  5395  fcoi1  5482  f1orel  5551  funbrfv  5644  funbrfv2b  5651  fvmptss2  5682  mptrcl  5690  elfvmptrab1  5702  funfvbrb  5721  fmptco  5774  funopsn  5790  funresdfunsnss  5815  elmpocl  6171  funexw  6227  mpoxopn0yelv  6355  tfrlem6  6432  funresdfunsndc  6622  pmresg  6793  fundmen  6929  caseinl  7226  caseinr  7227  axaddf  8023  axmulf  8024  hashinfom  10967  4sqlemffi  12885  structcnvcnv  13014  lidlmex  14404  istopon  14652  eltg4i  14694  eltg3  14696  tg1  14698  tg2  14699  tgclb  14704  lmrcl  14830  1vgrex  15786  edg0iedg0g  15831  umgrnloopv  15879