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

Theorem funrel 5821
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 5806 . 2 (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴𝐴) ⊆ I ))
21simplbi 475 1 (Fun 𝐴 → Rel 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3540   I cid 4948  ccnv 5037  ccom 5042  Rel wrel 5043  Fun wfun 5798
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 196  df-an 385  df-fun 5806
This theorem is referenced by:  funeu  5828  nfunv  5835  funopg  5836  funssres  5844  funun  5846  fununfun  5848  fununi  5878  funcnvres2  5883  fnrel  5903  fcoi1  5991  f1orel  6053  funbrfv  6144  funbrfv2b  6150  funfv2  6176  funfvbrb  6238  fimacnvinrn  6256  fvn0ssdmfun  6258  funopsn  6319  funresdfunsn  6360  wfrrel  7307  tfrlem6  7365  tfr2b  7379  pmresg  7771  fundmen  7916  resfifsupp  8186  rankwflemb  8539  gruima  9503  structcnvcnv  15706  inviso1  16249  setciso  16564  pmtrsn  17762  00lsp  18802  edg0iedg0  25800  constr3pthlem1  26183  0eusgraiff0rgracl  26468  fmptcof2  28839  fgreu  28854  bnj1379  30155  fundmpss  30910  funsseq  30912  frrlem5b  31029  frrlem6  31033  nofulllem3  31103  nofulllem5  31105  imageval  31207  imagesset  31230  cocnv  32690  frege124d  37072  frege129d  37074  frege133d  37076  funbrafv  39887  funbrafv2b  39888  edg0usgr  40479  usgr1v0edg  40483  rngciso  41774  rngcisoALTV  41786  ringciso  41825  ringcisoALTV  41849
  Copyright terms: Public domain W3C validator