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

Theorem dffn4 5806
Description: A function maps onto its range. (Contributed by NM, 10-May-1998.)
Assertion
Ref Expression
dffn4

Proof of Theorem dffn4
StepHypRef Expression
1 eqid 2457 . . 3
21biantru 505 . 2
3 df-fo 5599 . 2
42, 3bitr4i 252 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  =wceq 1395  rancrn 5005  Fnwfn 5588  -onto->wfo 5591
This theorem is referenced by:  funforn  5807  ffoss  6761  tposf2  6998  mapsn  7480  fidomdm  7822  pwfilem  7834  indexfi  7848  intrnfi  7896  fifo  7912  ixpiunwdom  8038  infpwfien  8464  infmap2  8619  cfflb  8660  cfslb2n  8669  ttukeylem6  8915  fnrndomg  8934  rankcf  9176  tskuni  9182  tskurn  9188  fseqsupcl  12087  vdwlem6  14504  0ram2  14539  0ramcl  14541  quslem  14940  gsumval3OLD  16908  gsumval3  16911  gsumzoppg  16967  gsumzoppgOLD  16968  mplsubrglem  18100  mplsubrglemOLD  18101  rncmp  19896  cmpsub  19900  tgcmp  19901  hauscmplem  19906  concn  19927  2ndcctbss  19956  2ndcomap  19959  2ndcsep  19960  comppfsc  20033  ptcnplem  20122  txtube  20141  txcmplem1  20142  tx1stc  20151  tx2ndc  20152  qtopid  20206  qtopcmplem  20208  qtopkgen  20211  kqtopon  20228  kqopn  20235  kqcld  20236  qtopf1  20317  rnelfm  20454  fmfnfmlem2  20456  fmfnfm  20459  alexsubALT  20551  ptcmplem2  20553  tmdgsum2  20595  tsmsxplem1  20655  met1stc  21024  met2ndci  21025  uniiccdif  21987  dyadmbl  22009  mbfimaopnlem  22062  i1fadd  22102  i1fmul  22103  itg1addlem4  22106  i1fmulc  22110  mbfi1fseqlem4  22125  limciun  22298  aannenlem3  22726  efabl  22937  logccv  23044  dmct  27537  locfinreflem  27843  mvrsfpw  28866  msrfo  28906  mtyf  28912  itg2addnclem2  30067  istotbnd3  30267  sstotbnd  30271  prdsbnd  30289  cntotbnd  30292  heiborlem1  30307  heibor  30317  dihintcl  37071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2449  df-fo 5599
  Copyright terms: Public domain W3C validator