Theorem funrel 6585

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

Syntax hints:   → wi 4   ⊆ wss 3963   I cid 5582  ^◡ccnv 5688   ∘ ccom 5693  Rel wrel 5694  Fun wfun 6557

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 6565

This theorem is referenced by:  0nelfun  6586  funeu  6593  nfunv  6601  funopg  6602  funssres  6612  funun  6614  fununfun  6616  fununi  6643  funcnvres2  6648  fnrel  6671  fcoi1  6783  f1orel  6852  funbrfv  6958  funbrfv2b  6966  funfv2  6997  funfvbrb  7071  fimacnvinrn  7091  fvn0ssdmfun  7094  funopsn  7168  funresdfunsn  7209  funexw  7975  funfv1st2nd  8070  funelss  8071  funeldmdif  8072  frrlem6  8315  wfrrelOLD  8353  tfrlem6  8421  tfr2b  8435  pmresg  8909  fundmen  9070  resfifsupp  9435  rankwflemb  9831  gruima  10840  structcnvcnv  17187  inviso1  17814  setciso  18145  rngciso  20655  ringciso  20689  nolt02o  27755  nogt01o  27756  nosupbnd1  27774  nosupbnd2lem1  27775  nosupbnd2  27776  noinfbnd1  27789  noinfbnd2lem1  27790  noinfbnd2  27791  noetasuplem2  27794  noetasuplem3  27795  noetasuplem4  27796  noetainflem2  27798  edg0iedg0  29087  edg0usgr  29285  usgr1v0edg  29289  fgreu  32689  fressupp  32703  gsumhashmul  33047  cycpmconjvlem  33144  cycpmconjslem2  33158  bnj1379  34823  funen1cnv  35081  fundmpss  35748  funsseq  35749  imageval  35912  imagesset  35935  cocnv  37712  frege124d  43751  frege129d  43753  frege133d  43755  funbrafv  47108  funbrafv2b  47109  funbrafv2  47197  isubgrvtxuhgr  47788  rngcisoALTV  48121  ringcisoALTV  48155  ackvalsuc0val  48537