Theorem funrel 6558

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

Syntax hints:   → wi 4   ⊆ wss 3931   I cid 5552  ^◡ccnv 5658   ∘ ccom 5663  Rel wrel 5664  Fun wfun 6530

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 207  df-an 396  df-fun 6538

This theorem is referenced by:  0nelfun  6559  funeu  6566  nfunv  6574  funopg  6575  funssres  6585  funun  6587  fununfun  6589  fununi  6616  funcnvres2  6621  fnrel  6645  fcoi1  6757  f1orel  6826  funbrfv  6932  funbrfv2b  6941  funfv2  6972  funfvbrb  7046  fimacnvinrn  7066  fvn0ssdmfun  7069  funopsn  7143  funresdfunsn  7186  funexw  7955  funfv1st2nd  8050  funelss  8051  funeldmdif  8052  frrlem6  8295  wfrrelOLD  8333  tfrlem6  8401  tfr2b  8415  pmresg  8889  fundmen  9050  resfifsupp  9414  rankwflemb  9812  gruima  10821  structcnvcnv  17177  inviso1  17784  setciso  18109  rngciso  20603  ringciso  20637  nolt02o  27664  nogt01o  27665  nosupbnd1  27683  nosupbnd2lem1  27684  nosupbnd2  27685  noinfbnd1  27698  noinfbnd2lem1  27699  noinfbnd2  27700  noetasuplem2  27703  noetasuplem3  27704  noetasuplem4  27705  noetainflem2  27707  edg0iedg0  29039  edg0usgr  29237  usgr1v0edg  29241  fgreu  32655  fressupp  32670  gsumhashmul  33060  cycpmconjvlem  33157  cycpmconjslem2  33171  bnj1379  34866  funen1cnv  35124  fundmpss  35789  funsseq  35790  imageval  35953  imagesset  35976  cocnv  37754  frege124d  43752  frege129d  43754  frege133d  43756  funbrafv  47154  funbrafv2b  47155  funbrafv2  47243  isubgrvtxuhgr  47844  rngcisoALTV  48219  ringcisoALTV  48253  ackvalsuc0val  48634