Theorem funrel 6554

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3902   I cid 5553  ^◡ccnv 5658   ∘ ccom 5663  Rel wrel 5664  Fun wfun 6531

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 6539

This theorem is used by:  0nelfun  6555  funeu  6562  nfunv  6570  funopg  6571  funssres  6581  funun  6583  fununfun  6585  fununi  6612  funcnvres2  6617  fnrel  6638  fcoi1  6753  f1orel  6824  funbrfv  6930  funbrfv2b  6939  funfv2  6970  funfvbrb  7047  fimacnvinrn  7068  fvn0ssdmfun  7071  funopsnOLD  7149  funexw  7953  funfv1st2nd  8047  funelss  8048  funeldmdif  8049  frrlem6  8294  tfrlem6OLD  8375  tfr2b  8389  pmresg  8881  funen1cnv  9039  fundmen  9042  rankwflemb  9779  gruima  10815  structcnvcnv  17251  inviso1  17861  setciso  18186  rngciso  20806  ringciso  20840  nolt02o  27939  nogt01o  27940  nosupbnd1  27958  nosupbnd2lem1  27959  nosupbnd2  27960  noinfbnd1  27973  noinfbnd2lem1  27974  noinfbnd2  27975  noetasuplem2  27978  noetasuplem3  27979  noetasuplem4  27980  noetainflem2  27982  edg0iedg0  29520  edg0usgr  29721  usgr1v0edg  29725  fgreu  33152  fressupp  33168  gsumhashmul  33515  cycpmconjvlem  33589  cycpmconjslem2  33603  bnj1379  35347  fundmpss  36354  funsseq  36355  imageval  36515  imagesset  36540  cocnv  38483  frege124d  44609  frege129d  44611  frege133d  44613  funbrafv  48054  funbrafv2b  48055  funbrafv2  48143  isubgrvtxuhgr  48788  rngcisoALTV  49200  ringcisoALTV  49234  ackvalsuc0val  49625