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

Theorem forn 5803
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 5599 . 2
21simprbi 464 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  rancrn 5005  Fnwfn 5588  -onto->wfo 5591
This theorem is referenced by:  dffo2  5804  foima  5805  fodmrnu  5808  f1imacnv  5837  foimacnv  5838  foun  5839  resdif  5841  fococnv2  5846  foelrni  5921  cbvfo  6192  isoini  6234  isofrlem  6236  isoselem  6237  canth  6254  f1opw2  6528  fornex  6769  wemoiso2  6786  curry1  6892  curry2  6895  bren  7545  en1  7602  fopwdom  7645  domss2  7696  mapen  7701  ssenen  7711  phplem4  7719  php3  7723  ssfi  7760  fodomfib  7820  f1opwfi  7844  ordiso2  7961  ordtypelem10  7973  oismo  7986  brwdom  8014  brwdom2  8020  wdomtr  8022  unxpwdom2  8035  wemapwe  8160  wemapweOLD  8161  infxpenc2lem1  8417  fseqen  8429  fodomfi2  8462  infpwfien  8464  infmap2  8619  ackbij2  8644  infpssr  8709  fodomb  8925  fpwwe2lem6  9034  fpwwe2lem9  9037  tskuni  9182  gruen  9211  hashfacen  12503  supcvg  13667  ruclem13  13975  unbenlem  14426  imasval  14908  imasaddfnlem  14925  imasvscafn  14934  imasless  14937  xpsfrn  14966  fulloppc  15291  imasmnd2  15957  imasgrp2  16185  oppglsm  16662  efgrelexlemb  16768  gsumzres  16914  gsumzcl2  16915  gsumzf1o  16917  gsumzresOLD  16918  gsumzclOLD  16919  gsumzf1oOLD  16920  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsumconst  16954  gsumzmhm  16957  gsumzmhmOLD  16958  gsumzoppg  16967  gsumzoppgOLD  16968  dprdf1o  17079  imasring  17268  gsumfsum  18484  zncyg  18587  znf1o  18590  znleval  18593  znunit  18602  cygznlem2a  18606  indlcim  18875  cmpfi  19908  cnconn  19923  1stcfb  19946  qtopval2  20197  basqtop  20212  tgqtop  20213  imastopn  20221  hmeontr  20270  hmeoqtop  20276  nrmhmph  20295  cmphaushmeo  20301  elfm3  20451  qustgpopn  20618  tsmsf1o  20647  imasf1oxmet  20878  imasf1omet  20879  imasf1oxms  20992  cnheiborlem  21454  ovolctb  21901  dyadmbl  22009  dvcnvrelem2  22419  dvcnvre  22420  efifo  22934  circgrp  22939  circsubm  22940  logrn  22946  dvrelog  23018  efopnlem2  23038  fsumdvdsmul  23471  f1otrg  24174  axcontlem10  24276  eupares  24975  eupath2lem3  24979  isgrpo  25198  isgrpoi  25200  isgrp2d  25237  isgrpda  25299  rngopidOLD  25325  opidon2OLD  25326  circgrpOLD  25376  rngmgmbs4  25419  pjrn  26625  ballotlemro  28461  erdsze2lem1  28647  cnpcon  28675  bdayrn  29437  mblfinlem2  30052  volsupnfl  30059  ismtyres  30304  dnnumch2  30991  lnmlmic  31034  pwslnmlem1  31038  pwslnmlem2  31039  stoweidlem27  31809  fourierdlem51  31940  fourierdlem102  31991  fourierdlem114  32003  mapdrn  37376
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 185  df-an 371  df-fo 5599
  Copyright terms: Public domain W3C validator