MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funrel Structured version   Visualization version   GIF version

Theorem funrel 6523
Description: A function is a relation. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
funrel (Fun 𝐴 → Rel 𝐴)

Proof of Theorem funrel
StepHypRef Expression
1 df-fun 6503 . 2 (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴𝐴) ⊆ I ))
21simplbi 499 1 (Fun 𝐴 → Rel 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3915   I cid 5535  ccnv 5637  ccom 5642  Rel wrel 5643  Fun wfun 6495
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 398  df-fun 6503
This theorem is referenced by:  0nelfun  6524  funeu  6531  nfunv  6539  funopg  6540  funssres  6550  funun  6552  fununfun  6554  fununi  6581  funcnvres2  6586  fnrel  6609  fcoi1  6721  f1orel  6792  funbrfv  6898  funbrfv2b  6905  funfv2  6934  funfvbrb  7006  fimacnvinrn  7027  fvn0ssdmfun  7030  funopsn  7099  funresdfunsn  7140  funexw  7889  funfv1st2nd  7983  funelss  7984  funeldmdif  7985  frrlem6  8227  wfrrelOLD  8265  tfrlem6  8333  tfr2b  8347  pmresg  8815  fundmen  8982  resfifsupp  9340  rankwflemb  9736  gruima  10745  structcnvcnv  17032  inviso1  17656  setciso  17984  nolt02o  27059  nogt01o  27060  nosupbnd1  27078  nosupbnd2lem1  27079  nosupbnd2  27080  noinfbnd1  27093  noinfbnd2lem1  27094  noinfbnd2  27095  noetasuplem2  27098  noetasuplem3  27099  noetasuplem4  27100  noetainflem2  27102  edg0iedg0  28048  edg0usgr  28243  usgr1v0edg  28247  fgreu  31630  fressupp  31645  gsumhashmul  31940  cycpmconjvlem  32032  cycpmconjslem2  32046  bnj1379  33482  funen1cnv  33732  fundmpss  34380  funsseq  34381  imageval  34544  imagesset  34567  cocnv  36213  frege124d  42107  frege129d  42109  frege133d  42111  funbrafv  45464  funbrafv2b  45465  funbrafv2  45553  rngciso  46354  rngcisoALTV  46366  ringciso  46405  ringcisoALTV  46429  ackvalsuc0val  46847
  Copyright terms: Public domain W3C validator