Theorem funrel 6534

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

Syntax hints:   → wi 4   ⊆ wss 3904   I cid 5539  ^◡ccnv 5644   ∘ ccom 5649  Rel wrel 5650  Fun wfun 6511

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 209  df-an 400  df-fun 6519

This theorem is referenced by:  0nelfun  6535  funeu  6542  nfunv  6550  funopg  6551  funssres  6561  funun  6563  fununfun  6565  fununi  6592  funcnvres2  6597  fnrel  6619  fcoi1  6734  f1orel  6805  funbrfv  6911  funbrfv2b  6920  funfv2  6951  funfvbrb  7028  fimacnvinrn  7048  fvn0ssdmfun  7051  funopsnOLD  7127  funexw  7929  funfv1st2nd  8023  funelss  8024  funeldmdif  8025  frrlem6  8267  tfrlem6OLD  8348  tfr2b  8362  pmresg  8848  fundmen  9008  rankwflemb  9748  gruima  10757  structcnvcnv  17172  inviso1  17782  setciso  18107  rngciso  20667  ringciso  20701  nolt02o  27736  nogt01o  27737  nosupbnd1  27755  nosupbnd2lem1  27756  nosupbnd2  27757  noinfbnd1  27770  noinfbnd2lem1  27771  noinfbnd2  27772  noetasuplem2  27775  noetasuplem3  27776  noetasuplem4  27777  noetainflem2  27779  edg0iedg0  29202  edg0usgr  29400  usgr1v0edg  29404  fgreu  32823  fressupp  32840  gsumhashmul  33208  cycpmconjvlem  33282  cycpmconjslem2  33296  bnj1379  35089  funen1cnv  35346  fundmpss  36081  funsseq  36082  imageval  36242  imagesset  36267  cocnv  38188  frege124d  44301  frege129d  44303  frege133d  44305  funbrafv  47716  funbrafv2b  47717  funbrafv2  47805  isubgrvtxuhgr  48450  rngcisoALTV  48863  ringcisoALTV  48897  ackvalsuc0val  49273