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  28346  edg0usgr  28541  usgr1v0edg  28545  fgreu  31928  fressupp  31941  gsumhashmul  32239  cycpmconjvlem  32331  cycpmconjslem2  32345  bnj1379  33872  funen1cnv  34122  fundmpss  34769  funsseq  34770  imageval  34933  imagesset  34956  cocnv  36641  frege124d  42560  frege129d  42562  frege133d  42564  funbrafv  45914  funbrafv2b  45915  funbrafv2  46003  rngciso  46928  rngcisoALTV  46940  ringciso  46979  ringcisoALTV  47003  ackvalsuc0val  47421