Theorem funrel 6556

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895   I cid 5544  ^◡ccnv 5649   ∘ ccom 5654  Rel wrel 5655  Fun wfun 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fun 6540

This theorem is used by:  0nelfun  6557  funeu  6565  nfunv  6573  funopg  6574  funssres  6584  funun  6586  fununfun  6588  fununi  6615  funcnvres2  6620  fnrel  6641  fcoi1  6756  f1orel  6827  funbrfv  6933  funbrfv2b  6942  funfv2  6973  funfvbrb  7050  fimacnvinrn  7071  fvn0ssdmfun  7074  funopsnOLD  7152  funexw  7964  funfv1st2nd  8057  funelss  8058  funeldmdif  8059  frrlem6  8312  tfrlem6OLD  8393  tfr2b  8407  pmresg  8901  funen1cnv  9059  fundmen  9062  rankwflembOLD  9804  gruima  10890  structcnvcnv  17336  inviso1  17946  setciso  18271  rngciso  20895  ringciso  20929  nolt02o  28057  nogt01o  28058  nosupbnd1  28076  nosupbnd2lem1  28077  nosupbnd2  28078  noinfbnd1  28091  noinfbnd2lem1  28092  noinfbnd2  28093  noetasuplem2  28096  noetasuplem3  28097  noetasuplem4  28098  noetainflem2  28100  edg0iedg0  29638  edg0usgr  29839  usgr1v0edg  29843  fgreu  33312  fressupp  33328  gsumhashmul  33674  cycpmconjvlem  33748  cycpmconjslem2  33762  bnj1379  35506  fundmpss  36624  funsseq  36625  imageval  36784  imagesset  36809  cocnv  38752  frege124d  44854  frege129d  44856  frege133d  44858  hfstructcan  46124  funbrafv  48321  funbrafv2b  48322  funbrafv2  48410  isubgrvtxuhgr  49055  rngcisoALTV  49467  ringcisoALTV  49501  ackvalsuc0val  49892