Theorem funrel 6449

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

Syntax hints:   → wi 4   ⊆ wss 3892   I cid 5489  ^◡ccnv 5589   ∘ ccom 5594  Rel wrel 5595  Fun wfun 6426

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 206  df-an 397  df-fun 6434

This theorem is referenced by:  0nelfun  6450  funeu  6457  nfunv  6465  funopg  6466  funssres  6476  funun  6478  fununfun  6480  fununi  6507  funcnvres2  6512  fnrel  6533  fcoi1  6646  f1orel  6717  funbrfv  6817  funbrfv2b  6824  funfv2  6853  funfvbrb  6925  fimacnvinrn  6946  fvn0ssdmfun  6949  funopsn  7017  funresdfunsn  7058  funexw  7788  funfv1st2nd  7880  funelss  7881  funeldmdif  7882  frrlem6  8098  wfrrelOLD  8136  tfrlem6  8204  tfr2b  8218  pmresg  8641  fundmen  8804  resfifsupp  9134  rankwflemb  9552  gruima  10559  structcnvcnv  16852  inviso1  17476  setciso  17804  edg0iedg0  27423  edg0usgr  27618  usgr1v0edg  27622  fgreu  31005  fressupp  31018  gsumhashmul  31312  cycpmconjvlem  31404  cycpmconjslem2  31418  bnj1379  32806  funen1cnv  33056  fundmpss  33736  funsseq  33738  nolt02o  33894  nogt01o  33895  nosupbnd1  33913  nosupbnd2lem1  33914  nosupbnd2  33915  noinfbnd1  33928  noinfbnd2lem1  33929  noinfbnd2  33930  noetasuplem2  33933  noetasuplem3  33934  noetasuplem4  33935  noetainflem2  33937  imageval  34228  imagesset  34251  cocnv  35879  frege124d  41339  frege129d  41341  frege133d  41343  funbrafv  44618  funbrafv2b  44619  funbrafv2  44707  rngciso  45509  rngcisoALTV  45521  ringciso  45560  ringcisoALTV  45584  ackvalsuc0val  46002