Theorem funrel 6517

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

Syntax hints:   → wi 4   ⊆ wss 3903   I cid 5526  ^◡ccnv 5631   ∘ ccom 5636  Rel wrel 5637  Fun wfun 6494

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 6502

This theorem is referenced by:  0nelfun  6518  funeu  6525  nfunv  6533  funopg  6534  funssres  6544  funun  6546  fununfun  6548  fununi  6575  funcnvres2  6580  fnrel  6602  fcoi1  6716  f1orel  6785  funbrfv  6890  funbrfv2b  6899  funfv2  6930  funfvbrb  7005  fimacnvinrn  7025  fvn0ssdmfun  7028  funopsn  7103  funresdfunsn  7145  funexw  7906  funfv1st2nd  8000  funelss  8001  funeldmdif  8002  frrlem6  8243  tfrlem6  8323  tfr2b  8337  pmresg  8820  fundmen  8980  resfifsupp  9312  rankwflemb  9717  gruima  10725  structcnvcnv  17092  inviso1  17702  setciso  18027  rngciso  20583  ringciso  20617  nolt02o  27675  nogt01o  27676  nosupbnd1  27694  nosupbnd2lem1  27695  nosupbnd2  27696  noinfbnd1  27709  noinfbnd2lem1  27710  noinfbnd2  27711  noetasuplem2  27714  noetasuplem3  27715  noetasuplem4  27716  noetainflem2  27718  edg0iedg0  29140  edg0usgr  29338  usgr1v0edg  29342  fgreu  32760  fressupp  32777  gsumhashmul  33160  cycpmconjvlem  33234  cycpmconjslem2  33248  bnj1379  35005  funen1cnv  35263  fundmpss  35980  funsseq  35981  imageval  36141  imagesset  36166  cocnv  37970  frege124d  44111  frege129d  44113  frege133d  44115  funbrafv  47512  funbrafv2b  47513  funbrafv2  47601  isubgrvtxuhgr  48218  rngcisoALTV  48631  ringcisoALTV  48665  ackvalsuc0val  49041