Theorem funrel 6468

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

Syntax hints:   → wi 4   ⊆ wss 3889   I cid 5490  ^◡ccnv 5590   ∘ ccom 5595  Rel wrel 5596  Fun wfun 6441

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 206  df-an 396  df-fun 6449

This theorem is referenced by:  0nelfun  6469  funeu  6476  nfunv  6484  funopg  6485  funssres  6495  funun  6497  fununfun  6499  fununi  6526  funcnvres2  6531  fnrel  6554  fcoi1  6666  f1orel  6737  funbrfv  6840  funbrfv2b  6847  funfv2  6876  funfvbrb  6948  fimacnvinrn  6969  fvn0ssdmfun  6972  funopsn  7040  funresdfunsn  7081  funexw  7814  funfv1st2nd  7907  funelss  7908  funeldmdif  7909  frrlem6  8127  wfrrelOLD  8165  tfrlem6  8233  tfr2b  8247  pmresg  8678  fundmen  8845  resfifsupp  9184  rankwflemb  9579  gruima  10586  structcnvcnv  16882  inviso1  17506  setciso  17834  edg0iedg0  27453  edg0usgr  27648  usgr1v0edg  27652  fgreu  31037  fressupp  31050  gsumhashmul  31344  cycpmconjvlem  31436  cycpmconjslem2  31450  bnj1379  32838  funen1cnv  33088  fundmpss  33768  funsseq  33770  nolt02o  33926  nogt01o  33927  nosupbnd1  33945  nosupbnd2lem1  33946  nosupbnd2  33947  noinfbnd1  33960  noinfbnd2lem1  33961  noinfbnd2  33962  noetasuplem2  33965  noetasuplem3  33966  noetasuplem4  33967  noetainflem2  33969  imageval  34260  imagesset  34283  cocnv  35911  frege124d  41393  frege129d  41395  frege133d  41397  funbrafv  44690  funbrafv2b  44691  funbrafv2  44779  rngciso  45580  rngcisoALTV  45592  ringciso  45631  ringcisoALTV  45655  ackvalsuc0val  46073