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

Theorem funrel 5500
 Description: A function is a relation. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
funrel

Proof of Theorem funrel
StepHypRef Expression
1 df-fun 5485 . 2
21simplbi 448 1
 Colors of variables: wff set class Syntax hints:   wi 4   wss 3306   cid 4522  ccnv 4906   ccom 4911   wrel 4912   wfun 5477 This theorem is referenced by:  funeu  5506  nfunv  5513  funopg  5514  funssres  5522  funun  5524  fununi  5546  funcnvres2  5553  fnrel  5572  fcoi1  5646  f1orel  5706  funbrfv  5794  funbrfv2b  5800  funfv2  5820  funfvbrb  5872  fmptco  5930  tfrlem6  6672  tfr2b  6686  pmresg  7070  fundmen  7209  rankwflemb  7748  gruima  8708  structcnvcnv  13511  inviso1  14022  setciso  14277  00lsp  16088  constr3pthlem1  21673  fimacnvinrn  24078  fmptcof2  24107  fundmpss  25421  funsseq  25424  wfrlem6  25574  frrlem5b  25618  frrlem6  25622  nofulllem3  25690  nofulllem5  25692  imageval  25806  imagesset  25829  cocnv  26465  funbrafv  28036  funbrafv2b  28037  bnj1379  29300 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 179  df-an 362  df-fun 5485
 Copyright terms: Public domain W3C validator