Theorem funrel 6563

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

Syntax hints:   → wi 4   ⊆ wss 3931   I cid 5557  ^◡ccnv 5664   ∘ ccom 5669  Rel wrel 5670  Fun wfun 6535

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 6543

This theorem is referenced by:  0nelfun  6564  funeu  6571  nfunv  6579  funopg  6580  funssres  6590  funun  6592  fununfun  6594  fununi  6621  funcnvres2  6626  fnrel  6650  fcoi1  6762  f1orel  6831  funbrfv  6937  funbrfv2b  6946  funfv2  6977  funfvbrb  7051  fimacnvinrn  7071  fvn0ssdmfun  7074  funopsn  7148  funresdfunsn  7191  funexw  7958  funfv1st2nd  8053  funelss  8054  funeldmdif  8055  frrlem6  8298  wfrrelOLD  8336  tfrlem6  8404  tfr2b  8418  pmresg  8892  fundmen  9053  resfifsupp  9419  rankwflemb  9815  gruima  10824  structcnvcnv  17172  inviso1  17781  setciso  18107  rngciso  20606  ringciso  20640  nolt02o  27676  nogt01o  27677  nosupbnd1  27695  nosupbnd2lem1  27696  nosupbnd2  27697  noinfbnd1  27710  noinfbnd2lem1  27711  noinfbnd2  27712  noetasuplem2  27715  noetasuplem3  27716  noetasuplem4  27717  noetainflem2  27719  edg0iedg0  29000  edg0usgr  29198  usgr1v0edg  29202  fgreu  32617  fressupp  32632  gsumhashmul  33003  cycpmconjvlem  33100  cycpmconjslem2  33114  bnj1379  34803  funen1cnv  35061  fundmpss  35726  funsseq  35727  imageval  35890  imagesset  35913  cocnv  37691  frege124d  43736  frege129d  43738  frege133d  43740  funbrafv  47128  funbrafv2b  47129  funbrafv2  47217  isubgrvtxuhgr  47808  rngcisoALTV  48151  ringcisoALTV  48185  ackvalsuc0val  48566