Theorem funrel 6503

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

Syntax hints:   → wi 4   ⊆ wss 3905   I cid 5517  ^◡ccnv 5622   ∘ ccom 5627  Rel wrel 5628  Fun wfun 6480

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 6488

This theorem is referenced by:  0nelfun  6504  funeu  6511  nfunv  6519  funopg  6520  funssres  6530  funun  6532  fununfun  6534  fununi  6561  funcnvres2  6566  fnrel  6588  fcoi1  6702  f1orel  6771  funbrfv  6875  funbrfv2b  6884  funfv2  6915  funfvbrb  6989  fimacnvinrn  7009  fvn0ssdmfun  7012  funopsn  7086  funresdfunsn  7129  funexw  7894  funfv1st2nd  7988  funelss  7989  funeldmdif  7990  frrlem6  8231  tfrlem6  8311  tfr2b  8325  pmresg  8804  fundmen  8963  resfifsupp  9306  rankwflemb  9708  gruima  10715  structcnvcnv  17082  inviso1  17691  setciso  18016  rngciso  20541  ringciso  20575  nolt02o  27623  nogt01o  27624  nosupbnd1  27642  nosupbnd2lem1  27643  nosupbnd2  27644  noinfbnd1  27657  noinfbnd2lem1  27658  noinfbnd2  27659  noetasuplem2  27662  noetasuplem3  27663  noetasuplem4  27664  noetainflem2  27666  edg0iedg0  29018  edg0usgr  29216  usgr1v0edg  29220  fgreu  32629  fressupp  32644  gsumhashmul  33027  cycpmconjvlem  33096  cycpmconjslem2  33110  bnj1379  34796  funen1cnv  35054  fundmpss  35739  funsseq  35740  imageval  35903  imagesset  35926  cocnv  37704  frege124d  43734  frege129d  43736  frege133d  43738  funbrafv  47143  funbrafv2b  47144  funbrafv2  47232  isubgrvtxuhgr  47849  rngcisoALTV  48262  ringcisoALTV  48296  ackvalsuc0val  48673