Theorem funrel 6555

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

Syntax hints:   → wi 4   ⊆ wss 3906   I cid 5557  ^◡ccnv 5662   ∘ ccom 5667  Rel wrel 5668  Fun wfun 6532

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 210  df-an 401  df-fun 6540

This theorem is referenced by:  0nelfun  6556  funeu  6563  nfunv  6571  funopg  6572  funssres  6582  funun  6584  fununfun  6586  fununi  6613  funcnvres2  6618  fnrel  6639  fcoi1  6754  f1orel  6825  funbrfv  6931  funbrfv2b  6940  funfv2  6971  funfvbrb  7048  fimacnvinrn  7068  fvn0ssdmfun  7071  funopsnOLD  7147  funexw  7950  funfv1st2nd  8044  funelss  8045  funeldmdif  8046  frrlem6  8289  tfrlem6OLD  8370  tfr2b  8384  pmresg  8869  fundmen  9029  rankwflemb  9766  gruima  10788  structcnvcnv  17214  inviso1  17824  setciso  18149  rngciso  20724  ringciso  20758  nolt02o  27837  nogt01o  27838  nosupbnd1  27856  nosupbnd2lem1  27857  nosupbnd2  27858  noinfbnd1  27871  noinfbnd2lem1  27872  noinfbnd2  27873  noetasuplem2  27876  noetasuplem3  27877  noetasuplem4  27878  noetainflem2  27880  edg0iedg0  29383  edg0usgr  29581  usgr1v0edg  29585  fgreu  32994  fressupp  33011  gsumhashmul  33365  cycpmconjvlem  33439  cycpmconjslem2  33453  bnj1379  35196  funen1cnv  35455  fundmpss  36237  funsseq  36238  imageval  36398  imagesset  36423  cocnv  38354  frege124d  44467  frege129d  44469  frege133d  44471  funbrafv  47872  funbrafv2b  47873  funbrafv2  47961  isubgrvtxuhgr  48606  rngcisoALTV  49019  ringcisoALTV  49053  ackvalsuc0val  49444