Theorem funrel 6509

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

Syntax hints:   → wi 4   ⊆ wss 3890   I cid 5518  ^◡ccnv 5623   ∘ ccom 5628  Rel wrel 5629  Fun wfun 6486

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 6494

This theorem is referenced by:  0nelfun  6510  funeu  6517  nfunv  6525  funopg  6526  funssres  6536  funun  6538  fununfun  6540  fununi  6567  funcnvres2  6572  fnrel  6594  fcoi1  6708  f1orel  6777  funbrfv  6882  funbrfv2b  6891  funfv2  6922  funfvbrb  6997  fimacnvinrn  7017  fvn0ssdmfun  7020  funopsn  7095  funresdfunsn  7137  funexw  7898  funfv1st2nd  7992  funelss  7993  funeldmdif  7994  frrlem6  8234  tfrlem6  8314  tfr2b  8328  pmresg  8811  fundmen  8971  resfifsupp  9303  rankwflemb  9708  gruima  10716  structcnvcnv  17114  inviso1  17724  setciso  18049  rngciso  20606  ringciso  20640  nolt02o  27673  nogt01o  27674  nosupbnd1  27692  nosupbnd2lem1  27693  nosupbnd2  27694  noinfbnd1  27707  noinfbnd2lem1  27708  noinfbnd2  27709  noetasuplem2  27712  noetasuplem3  27713  noetasuplem4  27714  noetainflem2  27716  edg0iedg0  29138  edg0usgr  29336  usgr1v0edg  29340  fgreu  32759  fressupp  32776  gsumhashmul  33143  cycpmconjvlem  33217  cycpmconjslem2  33231  bnj1379  34988  funen1cnv  35247  fundmpss  35965  funsseq  35966  imageval  36126  imagesset  36151  cocnv  38060  frege124d  44206  frege129d  44208  frege133d  44210  funbrafv  47618  funbrafv2b  47619  funbrafv2  47707  isubgrvtxuhgr  48352  rngcisoALTV  48765  ringcisoALTV  48799  ackvalsuc0val  49175