Theorem funrel 6583

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

Syntax hints:   → wi 4   ⊆ wss 3951   I cid 5577  ^◡ccnv 5684   ∘ ccom 5689  Rel wrel 5690  Fun wfun 6555

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 6563

This theorem is referenced by:  0nelfun  6584  funeu  6591  nfunv  6599  funopg  6600  funssres  6610  funun  6612  fununfun  6614  fununi  6641  funcnvres2  6646  fnrel  6670  fcoi1  6782  f1orel  6851  funbrfv  6957  funbrfv2b  6966  funfv2  6997  funfvbrb  7071  fimacnvinrn  7091  fvn0ssdmfun  7094  funopsn  7168  funresdfunsn  7209  funexw  7976  funfv1st2nd  8071  funelss  8072  funeldmdif  8073  frrlem6  8316  wfrrelOLD  8354  tfrlem6  8422  tfr2b  8436  pmresg  8910  fundmen  9071  resfifsupp  9437  rankwflemb  9833  gruima  10842  structcnvcnv  17190  inviso1  17810  setciso  18136  rngciso  20638  ringciso  20672  nolt02o  27740  nogt01o  27741  nosupbnd1  27759  nosupbnd2lem1  27760  nosupbnd2  27761  noinfbnd1  27774  noinfbnd2lem1  27775  noinfbnd2  27776  noetasuplem2  27779  noetasuplem3  27780  noetasuplem4  27781  noetainflem2  27783  edg0iedg0  29072  edg0usgr  29270  usgr1v0edg  29274  fgreu  32682  fressupp  32697  gsumhashmul  33064  cycpmconjvlem  33161  cycpmconjslem2  33175  bnj1379  34844  funen1cnv  35102  fundmpss  35767  funsseq  35768  imageval  35931  imagesset  35954  cocnv  37732  frege124d  43774  frege129d  43776  frege133d  43778  funbrafv  47170  funbrafv2b  47171  funbrafv2  47259  isubgrvtxuhgr  47850  rngcisoALTV  48193  ringcisoALTV  48227  ackvalsuc0val  48608