Theorem funrel 6515

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

Syntax hints:   → wi 4   ⊆ wss 3889   I cid 5525  ^◡ccnv 5630   ∘ ccom 5635  Rel wrel 5636  Fun wfun 6492

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 6500

This theorem is referenced by:  0nelfun  6516  funeu  6523  nfunv  6531  funopg  6532  funssres  6542  funun  6544  fununfun  6546  fununi  6573  funcnvres2  6578  fnrel  6600  fcoi1  6714  f1orel  6783  funbrfv  6888  funbrfv2b  6897  funfv2  6928  funfvbrb  7003  fimacnvinrn  7023  fvn0ssdmfun  7026  funopsnOLD  7102  funresdfunsn  7144  funexw  7905  funfv1st2nd  7999  funelss  8000  funeldmdif  8001  frrlem6  8241  tfrlem6  8321  tfr2b  8335  pmresg  8818  fundmen  8978  resfifsupp  9310  rankwflemb  9717  gruima  10725  structcnvcnv  17123  inviso1  17733  setciso  18058  rngciso  20615  ringciso  20649  nolt02o  27659  nogt01o  27660  nosupbnd1  27678  nosupbnd2lem1  27679  nosupbnd2  27680  noinfbnd1  27693  noinfbnd2lem1  27694  noinfbnd2  27695  noetasuplem2  27698  noetasuplem3  27699  noetasuplem4  27700  noetainflem2  27702  edg0iedg0  29124  edg0usgr  29322  usgr1v0edg  29326  fgreu  32744  fressupp  32761  gsumhashmul  33128  cycpmconjvlem  33202  cycpmconjslem2  33216  bnj1379  34972  funen1cnv  35231  fundmpss  35949  funsseq  35950  imageval  36110  imagesset  36135  cocnv  38046  frege124d  44188  frege129d  44190  frege133d  44192  funbrafv  47606  funbrafv2b  47607  funbrafv2  47695  isubgrvtxuhgr  48340  rngcisoALTV  48753  ringcisoALTV  48787  ackvalsuc0val  49163