Theorem funrel 6560

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3908   I cid 5560  ^◡ccnv 5665   ∘ ccom 5670  Rel wrel 5671  Fun wfun 6537

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 6545

This theorem is used by:  0nelfun  6561  funeu  6568  nfunv  6576  funopg  6577  funssres  6587  funun  6589  fununfun  6591  fununi  6618  funcnvres2  6623  fnrel  6644  fcoi1  6759  f1orel  6830  funbrfv  6936  funbrfv2b  6945  funfv2  6976  funfvbrb  7053  fimacnvinrn  7073  fvn0ssdmfun  7076  funopsnOLD  7152  funexw  7958  funfv1st2nd  8052  funelss  8053  funeldmdif  8054  frrlem6  8297  tfrlem6OLD  8378  tfr2b  8392  pmresg  8877  funen1cnv  9035  fundmen  9038  rankwflemb  9775  gruima  10805  structcnvcnv  17238  inviso1  17848  setciso  18173  rngciso  20774  ringciso  20808  nolt02o  27896  nogt01o  27897  nosupbnd1  27915  nosupbnd2lem1  27916  nosupbnd2  27917  noinfbnd1  27930  noinfbnd2lem1  27931  noinfbnd2  27932  noetasuplem2  27935  noetasuplem3  27936  noetasuplem4  27937  noetainflem2  27939  edg0iedg0  29442  edg0usgr  29640  usgr1v0edg  29644  fgreu  33053  fressupp  33070  gsumhashmul  33418  cycpmconjvlem  33492  cycpmconjslem2  33506  bnj1379  35250  fundmpss  36280  funsseq  36281  imageval  36441  imagesset  36466  cocnv  38417  frege124d  44528  frege129d  44530  frege133d  44532  funbrafv  47936  funbrafv2b  47937  funbrafv2  48025  isubgrvtxuhgr  48670  rngcisoALTV  49083  ringcisoALTV  49117  ackvalsuc0val  49508