Theorem funrel 6509

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

Syntax hints:   → wi 4   ⊆ wss 3901   I cid 5518  ^◡ccnv 5623   ∘ ccom 5628  Rel wrel 5629  Fun wfun 6486

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 6494

This theorem is referenced by:  0nelfun  6510  funeu  6517  nfunv  6525  funopg  6526  funssres  6536  funun  6538  fununfun  6540  fununi  6567  funcnvres2  6572  fnrel  6594  fcoi1  6708  f1orel  6777  funbrfv  6882  funbrfv2b  6891  funfv2  6922  funfvbrb  6996  fimacnvinrn  7016  fvn0ssdmfun  7019  funopsn  7093  funresdfunsn  7135  funexw  7896  funfv1st2nd  7990  funelss  7991  funeldmdif  7992  frrlem6  8233  tfrlem6  8313  tfr2b  8327  pmresg  8808  fundmen  8968  resfifsupp  9300  rankwflemb  9705  gruima  10713  structcnvcnv  17080  inviso1  17690  setciso  18015  rngciso  20571  ringciso  20605  nolt02o  27663  nogt01o  27664  nosupbnd1  27682  nosupbnd2lem1  27683  nosupbnd2  27684  noinfbnd1  27697  noinfbnd2lem1  27698  noinfbnd2  27699  noetasuplem2  27702  noetasuplem3  27703  noetasuplem4  27704  noetainflem2  27706  edg0iedg0  29128  edg0usgr  29326  usgr1v0edg  29330  fgreu  32750  fressupp  32767  gsumhashmul  33150  cycpmconjvlem  33223  cycpmconjslem2  33237  bnj1379  34986  funen1cnv  35244  fundmpss  35961  funsseq  35962  imageval  36122  imagesset  36147  cocnv  37922  frege124d  43998  frege129d  44000  frege133d  44002  funbrafv  47400  funbrafv2b  47401  funbrafv2  47489  isubgrvtxuhgr  48106  rngcisoALTV  48519  ringcisoALTV  48553  ackvalsuc0val  48929