Theorem funrel 6571

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

Syntax hints:   → wi 4   ⊆ wss 3944   I cid 5575  ^◡ccnv 5677   ∘ ccom 5682  Rel wrel 5683  Fun wfun 6543

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 395  df-fun 6551

This theorem is referenced by:  0nelfun  6572  funeu  6579  nfunv  6587  funopg  6588  funssres  6598  funun  6600  fununfun  6602  fununi  6629  funcnvres2  6634  fnrel  6657  fcoi1  6771  f1orel  6841  funbrfv  6947  funbrfv2b  6955  funfv2  6985  funfvbrb  7059  fimacnvinrn  7080  fvn0ssdmfun  7083  funopsn  7157  funresdfunsn  7198  funexw  7956  funfv1st2nd  8051  funelss  8052  funeldmdif  8053  frrlem6  8297  wfrrelOLD  8335  tfrlem6  8403  tfr2b  8417  pmresg  8889  fundmen  9056  resfifsupp  9422  rankwflemb  9818  gruima  10827  structcnvcnv  17125  inviso1  17752  setciso  18083  rngciso  20583  ringciso  20617  nolt02o  27674  nogt01o  27675  nosupbnd1  27693  nosupbnd2lem1  27694  nosupbnd2  27695  noinfbnd1  27708  noinfbnd2lem1  27709  noinfbnd2  27710  noetasuplem2  27713  noetasuplem3  27714  noetasuplem4  27715  noetainflem2  27717  edg0iedg0  28940  edg0usgr  29138  usgr1v0edg  29142  fgreu  32539  fressupp  32550  gsumhashmul  32860  cycpmconjvlem  32954  cycpmconjslem2  32968  bnj1379  34589  funen1cnv  34839  fundmpss  35490  funsseq  35491  imageval  35654  imagesset  35677  cocnv  37326  frege124d  43330  frege129d  43332  frege133d  43334  funbrafv  46673  funbrafv2b  46674  funbrafv2  46762  isubgrvtxuhgr  47333  rngcisoALTV  47522  ringcisoALTV  47556  ackvalsuc0val  47943