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 3890   I cid 5519  ^◡ccnv 5624   ∘ ccom 5629  Rel wrel 5630  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 208  df-an 397  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  6999  fimacnvinrn  7019  fvn0ssdmfun  7022  funopsnOLD  7098  funresdfunsn  7140  funexw  7901  funfv1st2nd  7995  funelss  7996  funeldmdif  7997  frrlem6  8238  tfrlem6  8318  tfr2b  8332  pmresg  8815  fundmen  8975  resfifsupp  9307  rankwflemb  9715  gruima  10723  structcnvcnv  17121  inviso1  17731  setciso  18056  rngciso  20617  ringciso  20651  nolt02o  27684  nogt01o  27685  nosupbnd1  27703  nosupbnd2lem1  27704  nosupbnd2  27705  noinfbnd1  27718  noinfbnd2lem1  27719  noinfbnd2  27720  noetasuplem2  27723  noetasuplem3  27724  noetasuplem4  27725  noetainflem2  27727  edg0iedg0  29149  edg0usgr  29347  usgr1v0edg  29351  fgreu  32770  fressupp  32787  gsumhashmul  33155  cycpmconjvlem  33229  cycpmconjslem2  33243  bnj1379  35019  funen1cnv  35276  fundmpss  36002  funsseq  36003  imageval  36163  imagesset  36188  cocnv  38099  frege124d  44212  frege129d  44214  frege133d  44216  funbrafv  47628  funbrafv2b  47629  funbrafv2  47717  isubgrvtxuhgr  48362  rngcisoALTV  48775  ringcisoALTV  48809  ackvalsuc0val  49185