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

Theorem forn 5593
Description: The codomain of an onto function is its range. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
forn

Proof of Theorem forn
StepHypRef Expression
1 df-fo 5396 . 2
21simprbi 454 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1687  rancrn 4812  Fnwfn 5385  -onto->wfo 5388
This theorem is referenced by:  dffo2  5594  foima  5595  fodmrnu  5598  f1imacnv  5627  foimacnv  5628  foun  5629  resdif  5631  fococnv2  5636  cbvfo  5961  isoini  5997  isofrlem  5999  isoselem  6000  canth  6017  f1opw2  6283  fornex  6515  wemoiso2  6532  curry1  6633  curry2  6636  bren  7278  en1  7335  fopwdom  7378  domss2  7429  mapen  7434  ssenen  7444  phplem4  7452  php3  7456  ssfi  7492  fodomfib  7550  f1opwfi  7574  ordiso2  7676  ordtypelem10  7688  oismo  7701  brwdom  7729  brwdom2  7735  wdomtr  7737  unxpwdom2  7750  wemapwe  7875  wemapweOLD  7876  infxpenc2lem1  8132  fseqen  8144  fodomfi2  8177  infpwfien  8179  infmap2  8334  ackbij2  8359  infpssr  8424  fodomb  8640  fpwwe2lem6  8748  fpwwe2lem9  8751  tskuni  8896  gruen  8925  hashfacen  12148  supcvg  13258  ruclem13  13464  unbenlem  13909  imasval  14389  imasaddfnlem  14406  imasvscafn  14415  imasless  14418  xpsfrn  14447  fulloppc  14772  imasmnd2  15398  imasgrp2  15607  oppglsm  16078  efgrelexlemb  16184  gsumzres  16320  gsumzcl  16321  gsumzf1o  16322  gsumzaddlem  16329  gsumconst  16336  gsumzmhm  16337  gsumzoppg  16343  dprdf1o  16399  imasrng  16535  gsumfsum  17589  zncyg  17689  znf1o  17692  znleval  17695  znunit  17704  cygznlem2a  17708  indlcim  17968  cmpfi  18715  cnconn  18730  1stcfb  18753  qtopval2  18973  basqtop  18988  tgqtop  18989  imastopn  18997  hmeontr  19046  hmeoqtop  19052  nrmhmph  19071  cmphaushmeo  19077  elfm3  19227  divstgpopn  19394  tsmsf1o  19419  imasf1oxmet  19650  imasf1omet  19651  imasf1oxms  19764  cnheiborlem  20226  ovolctb  20673  dyadmbl  20780  dvcnvrelem2  21190  dvcnvre  21191  efifo  21744  logrn  21751  dvrelog  21823  efopnlem2  21843  fsumdvdsmul  22276  f1otrg  22796  axcontlem10  22898  eupares  23275  eupath2lem3  23279  isgrpo  23362  isgrpoi  23364  isgrp2d  23401  isgrpda  23463  rngopid  23489  opidon2  23490  circgrp  23540  rngmgmbs4  23583  pjrn  24789  ballotlemro  26608  erdsze2lem1  26794  cnpcon  26822  bdayrn  27520  mblfinlem2  28100  volsupnfl  28107  ismtyres  28378  dnnumch2  29071  lnmlmic  29114  pwslnmlem1  29118  pwslnmlem2  29119  stoweidlem27  29496  gsumXzres  30467  gsumXzcl2  30468  gsumXzf1o  30470  gsumXzaddlem  30478  gsumXconst  30484  gsumXzmhm  30485  gsumXzoppg  30491  mapdrn  34731
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 364  df-fo 5396
  Copyright terms: Public domain W3C validator