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

Theorem forn 5640
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 5444 . 2
21simprbi 452 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  =wceq 1670  rancrn 4863  Fnwfn 5433  -onto->wfo 5436
This theorem is referenced by:  dffo2  5641  foima  5642  fodmrnu  5645  f1imacnv  5674  foimacnv  5675  foun  5676  resdif  5678  fococnv2  5683  cbvfo  6003  isoini  6039  isofrlem  6041  isoselem  6042  canth  6059  f1opw2  6323  fornex  6553  wemoiso2  6569  curry1  6670  curry2  6673  bren  7281  en1  7338  fopwdom  7381  domss2  7431  mapen  7436  ssenen  7446  phplem4  7454  php3  7458  ssfi  7494  fodomfib  7552  f1opwfi  7577  ordiso2  7651  ordtypelem10  7663  oismo  7676  brwdom  7702  brwdom2  7708  wdomtr  7710  unxpwdom2  7723  wemapwe  7821  infxpenc2lem1  8071  fseqen  8079  fodomfi2  8112  infpwfien  8114  infmap2  8269  ackbij2  8294  infpssr  8359  fodomb  8575  fpwwe2lem6  8681  fpwwe2lem9  8684  tskuni  8829  gruen  8858  hashfacen  12054  supcvg  13165  ruclem13  13371  unbenlem  13816  imasval  14291  imasaddfnlem  14307  imasvscafn  14316  imasless  14319  xpsfrn  14348  fulloppc  14673  imasmnd2  15298  imasgrp2  15504  oppglsm  15885  efgrelexlemb  15991  gsumzres  16127  gsumzcl  16128  gsumzf1o  16129  gsumzaddlem  16136  gsumconst  16142  gsumzmhm  16143  gsumzoppg  16149  dprdf1o  16205  imasrng  16341  gsumfsum  17391  zncyg  17454  znf1o  17457  znleval  17460  znunit  17469  cygznlem2a  17473  cmpfi  18485  cnconn  18500  1stcfb  18523  qtopval2  18743  basqtop  18758  tgqtop  18759  imastopn  18767  hmeontr  18816  hmeoqtop  18822  nrmhmph  18841  cmphaushmeo  18847  elfm3  18997  divstgpopn  19164  tsmsf1o  19189  imasf1oxmet  19420  imasf1omet  19421  imasf1oxms  19534  cnheiborlem  19994  ovolctb  20401  dyadmbl  20507  dvcnvrelem2  20917  dvcnvre  20918  efifo  21469  logrn  21476  dvrelog  21548  efopnlem2  21568  fsumdvdsmul  22001  eupares  22718  eupath2lem3  22722  isgrpo  22805  isgrpoi  22807  isgrp2d  22844  isgrpda  22906  rngopid  22932  opidon2  22933  circgrp  22983  rngmgmbs4  23026  pjrn  24232  ballotlemro  26055  erdsze2lem1  26237  cnpcon  26265  bdayrn  26971  axcontlem10  27251  mblfinlem2  27609  volsupnfl  27616  ismtyres  27889  dnnumch2  28546  lnmlmic  28589  pwslnmlem1  28593  pwslnmlem2  28594  indlcim  28650  stoweidlem27  29001  mapdrn  33997
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-fo 5444
  Copyright terms: Public domain W3C validator