Theorem funrel 6375

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

Syntax hints:   → wi 4   ⊆ wss 3853   I cid 5439  ^◡ccnv 5535   ∘ ccom 5540  Rel wrel 5541  Fun wfun 6352

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 400  df-fun 6360

This theorem is referenced by:  0nelfun  6376  funeu  6383  nfunv  6391  funopg  6392  funssres  6402  funun  6404  fununfun  6406  fununi  6433  funcnvres2  6438  fnrel  6458  fcoi1  6571  f1orel  6642  funbrfv  6741  funbrfv2b  6748  funfv2  6777  funfvbrb  6849  fimacnvinrn  6870  fvn0ssdmfun  6873  funopsn  6941  funresdfunsn  6982  funexw  7703  funfv1st2nd  7795  funelss  7796  funeldmdif  7797  frrlem6  8010  wfrrel  8038  tfrlem6  8096  tfr2b  8110  pmresg  8529  fundmen  8686  resfifsupp  8991  rankwflemb  9374  gruima  10381  structcnvcnv  16680  inviso1  17225  setciso  17551  edg0iedg0  27100  edg0usgr  27295  usgr1v0edg  27299  fgreu  30683  fressupp  30696  gsumhashmul  30989  cycpmconjvlem  31081  cycpmconjslem2  31095  bnj1379  32477  funen1cnv  32727  fundmpss  33410  funsseq  33412  nolt02o  33584  nogt01o  33585  nosupbnd1  33603  nosupbnd2lem1  33604  nosupbnd2  33605  noinfbnd1  33618  noinfbnd2lem1  33619  noinfbnd2  33620  noetasuplem2  33623  noetasuplem3  33624  noetasuplem4  33625  noetainflem2  33627  imageval  33918  imagesset  33941  cocnv  35569  frege124d  40987  frege129d  40989  frege133d  40991  funbrafv  44265  funbrafv2b  44266  funbrafv2  44354  rngciso  45156  rngcisoALTV  45168  ringciso  45207  ringcisoALTV  45231  ackvalsuc0val  45649