Theorem funrel 6435

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

Syntax hints:   → wi 4   ⊆ wss 3883   I cid 5479  ^◡ccnv 5579   ∘ ccom 5584  Rel wrel 5585  Fun wfun 6412

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 6420

This theorem is referenced by:  0nelfun  6436  funeu  6443  nfunv  6451  funopg  6452  funssres  6462  funun  6464  fununfun  6466  fununi  6493  funcnvres2  6498  fnrel  6519  fcoi1  6632  f1orel  6703  funbrfv  6802  funbrfv2b  6809  funfv2  6838  funfvbrb  6910  fimacnvinrn  6931  fvn0ssdmfun  6934  funopsn  7002  funresdfunsn  7043  funexw  7768  funfv1st2nd  7860  funelss  7861  funeldmdif  7862  frrlem6  8078  wfrrelOLD  8116  tfrlem6  8184  tfr2b  8198  pmresg  8616  fundmen  8775  resfifsupp  9086  rankwflemb  9482  gruima  10489  structcnvcnv  16782  inviso1  17395  setciso  17722  edg0iedg0  27328  edg0usgr  27523  usgr1v0edg  27527  fgreu  30911  fressupp  30924  gsumhashmul  31218  cycpmconjvlem  31310  cycpmconjslem2  31324  bnj1379  32710  funen1cnv  32960  fundmpss  33646  funsseq  33648  nolt02o  33825  nogt01o  33826  nosupbnd1  33844  nosupbnd2lem1  33845  nosupbnd2  33846  noinfbnd1  33859  noinfbnd2lem1  33860  noinfbnd2  33861  noetasuplem2  33864  noetasuplem3  33865  noetasuplem4  33866  noetainflem2  33868  imageval  34159  imagesset  34182  cocnv  35810  frege124d  41258  frege129d  41260  frege133d  41262  funbrafv  44537  funbrafv2b  44538  funbrafv2  44626  rngciso  45428  rngcisoALTV  45440  ringciso  45479  ringcisoALTV  45503  ackvalsuc0val  45921