Theorem funrel 6503

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

Syntax hints:   → wi 4   ⊆ wss 3898   I cid 5513  ^◡ccnv 5618   ∘ ccom 5623  Rel wrel 5624  Fun wfun 6480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-fun 6488

This theorem is referenced by:  0nelfun  6504  funeu  6511  nfunv  6519  funopg  6520  funssres  6530  funun  6532  fununfun  6534  fununi  6561  funcnvres2  6566  fnrel  6588  fcoi1  6702  f1orel  6771  funbrfv  6876  funbrfv2b  6885  funfv2  6916  funfvbrb  6990  fimacnvinrn  7010  fvn0ssdmfun  7013  funopsn  7087  funresdfunsn  7129  funexw  7890  funfv1st2nd  7984  funelss  7985  funeldmdif  7986  frrlem6  8227  tfrlem6  8307  tfr2b  8321  pmresg  8800  fundmen  8960  resfifsupp  9288  rankwflemb  9693  gruima  10700  structcnvcnv  17066  inviso1  17675  setciso  18000  rngciso  20555  ringciso  20589  nolt02o  27635  nogt01o  27636  nosupbnd1  27654  nosupbnd2lem1  27655  nosupbnd2  27656  noinfbnd1  27669  noinfbnd2lem1  27670  noinfbnd2  27671  noetasuplem2  27674  noetasuplem3  27675  noetasuplem4  27676  noetainflem2  27678  edg0iedg0  29035  edg0usgr  29233  usgr1v0edg  29237  fgreu  32656  fressupp  32673  gsumhashmul  33048  cycpmconjvlem  33117  cycpmconjslem2  33131  bnj1379  34863  funen1cnv  35121  fundmpss  35832  funsseq  35833  imageval  35993  imagesset  36018  cocnv  37785  frege124d  43878  frege129d  43880  frege133d  43882  funbrafv  47282  funbrafv2b  47283  funbrafv2  47371  isubgrvtxuhgr  47988  rngcisoALTV  48401  ringcisoALTV  48435  ackvalsuc0val  48812