Theorem funrel 6523

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

Syntax hints:   → wi 4   ⊆ wss 3913   I cid 5535  ^◡ccnv 5637   ∘ ccom 5642  Rel wrel 5643  Fun wfun 6495

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 397  df-fun 6503

This theorem is referenced by:  0nelfun  6524  funeu  6531  nfunv  6539  funopg  6540  funssres  6550  funun  6552  fununfun  6554  fununi  6581  funcnvres2  6586  fnrel  6609  fcoi1  6721  f1orel  6792  funbrfv  6898  funbrfv2b  6905  funfv2  6934  funfvbrb  7006  fimacnvinrn  7027  fvn0ssdmfun  7030  funopsn  7099  funresdfunsn  7140  funexw  7889  funfv1st2nd  7983  funelss  7984  funeldmdif  7985  frrlem6  8227  wfrrelOLD  8265  tfrlem6  8333  tfr2b  8347  pmresg  8815  fundmen  8982  resfifsupp  9342  rankwflemb  9738  gruima  10747  structcnvcnv  17036  inviso1  17663  setciso  17991  nolt02o  27080  nogt01o  27081  nosupbnd1  27099  nosupbnd2lem1  27100  nosupbnd2  27101  noinfbnd1  27114  noinfbnd2lem1  27115  noinfbnd2  27116  noetasuplem2  27119  noetasuplem3  27120  noetasuplem4  27121  noetainflem2  27123  edg0iedg0  28069  edg0usgr  28264  usgr1v0edg  28268  fgreu  31655  fressupp  31670  gsumhashmul  31968  cycpmconjvlem  32060  cycpmconjslem2  32074  bnj1379  33531  funen1cnv  33781  fundmpss  34427  funsseq  34428  imageval  34591  imagesset  34614  cocnv  36257  frege124d  42155  frege129d  42157  frege133d  42159  funbrafv  45510  funbrafv2b  45511  funbrafv2  45599  rngciso  46400  rngcisoALTV  46412  ringciso  46451  ringcisoALTV  46475  ackvalsuc0val  46893