Theorem funrel 6566

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

Syntax hints:   → wi 4   ⊆ wss 3949   I cid 5574  ^◡ccnv 5676   ∘ ccom 5681  Rel wrel 5682  Fun wfun 6538

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 398  df-fun 6546

This theorem is referenced by:  0nelfun  6567  funeu  6574  nfunv  6582  funopg  6583  funssres  6593  funun  6595  fununfun  6597  fununi  6624  funcnvres2  6629  fnrel  6652  fcoi1  6766  f1orel  6837  funbrfv  6943  funbrfv2b  6950  funfv2  6980  funfvbrb  7053  fimacnvinrn  7074  fvn0ssdmfun  7077  funopsn  7146  funresdfunsn  7187  funexw  7938  funfv1st2nd  8032  funelss  8033  funeldmdif  8034  frrlem6  8276  wfrrelOLD  8314  tfrlem6  8382  tfr2b  8396  pmresg  8864  fundmen  9031  resfifsupp  9392  rankwflemb  9788  gruima  10797  structcnvcnv  17086  inviso1  17713  setciso  18041  nolt02o  27198  nogt01o  27199  nosupbnd1  27217  nosupbnd2lem1  27218  nosupbnd2  27219  noinfbnd1  27232  noinfbnd2lem1  27233  noinfbnd2  27234  noetasuplem2  27237  noetasuplem3  27238  noetasuplem4  27239  noetainflem2  27241  edg0iedg0  28315  edg0usgr  28510  usgr1v0edg  28514  fgreu  31897  fressupp  31910  gsumhashmul  32208  cycpmconjvlem  32300  cycpmconjslem2  32314  bnj1379  33841  funen1cnv  34091  fundmpss  34738  funsseq  34739  imageval  34902  imagesset  34925  cocnv  36593  frege124d  42512  frege129d  42514  frege133d  42516  funbrafv  45866  funbrafv2b  45867  funbrafv2  45955  rngciso  46880  rngcisoALTV  46892  ringciso  46931  ringcisoALTV  46955  ackvalsuc0val  47373