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

Theorem forn 5656
Description: The codomain of an onto function is its range. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
forn  |-  ( F : A -onto-> B  ->  ran  F  =  B )

Proof of Theorem forn
StepHypRef Expression
1 df-fo 5460 . 2  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
21simprbi 451 1  |-  ( F : A -onto-> B  ->  ran  F  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   ran crn 4879    Fn wfn 5449   -onto->wfo 5452
This theorem is referenced by:  dffo2  5657  foima  5658  fodmrnu  5661  f1imacnv  5691  foimacnv  5692  foun  5693  resdif  5696  fococnv2  5701  fornex  5970  cbvfo  6022  isoini  6058  isofrlem  6060  isoselem  6061  wemoiso2  6079  f1opw2  6298  curry1  6438  curry2  6441  canth  6539  bren  7117  en1  7174  fopwdom  7216  domss2  7266  mapen  7271  ssenen  7281  phplem4  7289  php3  7293  ssfi  7329  fodomfib  7386  f1opwfi  7410  ordiso2  7484  ordtypelem10  7496  oismo  7509  brwdom  7535  brwdom2  7541  wdomtr  7543  unxpwdom2  7556  wemapwe  7654  infxpenc2lem1  7900  fseqen  7908  fodomfi2  7941  infpwfien  7943  infmap2  8098  ackbij2  8123  infpssr  8188  fodomb  8404  fpwwe2lem6  8510  fpwwe2lem9  8513  tskuni  8658  gruen  8687  hashfacen  11703  supcvg  12635  ruclem13  12841  unbenlem  13276  imasval  13737  imasaddfnlem  13753  imasvscafn  13762  imasless  13765  xpsfrn  13794  fulloppc  14119  imasmnd2  14732  imasgrp2  14933  oppglsm  15276  efgrelexlemb  15382  gsumzres  15517  gsumzcl  15518  gsumzf1o  15519  gsumzaddlem  15526  gsumconst  15532  gsumzmhm  15533  gsumzoppg  15539  dprdf1o  15590  imasrng  15725  gsumfsum  16766  zncyg  16829  znf1o  16832  znleval  16835  znunit  16844  cygznlem2a  16848  cmpfi  17471  cnconn  17485  1stcfb  17508  qtopval2  17728  basqtop  17743  tgqtop  17744  imastopn  17752  hmeontr  17801  hmeoqtop  17807  nrmhmph  17826  cmphaushmeo  17832  elfm3  17982  divstgpopn  18149  tsmsf1o  18174  imasf1oxmet  18405  imasf1omet  18406  imasf1oxms  18519  cnheiborlem  18979  ovolctb  19386  dyadmbl  19492  dvcnvrelem2  19902  dvcnvre  19903  efifo  20449  logrn  20456  dvrelog  20528  efopnlem2  20548  fsumdvdsmul  20980  eupares  21697  eupath2lem3  21701  isgrpo  21784  isgrpoi  21786  isgrp2d  21823  isgrpda  21885  rngopid  21911  opidon2  21912  circgrp  21962  rngmgmbs4  22005  pjrn  23209  ballotlemro  24780  erdsze2lem1  24889  cnpcon  24917  bdayrn  25632  axcontlem10  25912  mblfinlem2  26244  volsupnfl  26251  ismtyres  26517  dnnumch2  27120  lnmlmic  27163  pwslnmlem1  27171  pwslnmlem2  27172  indlcim  27287  stoweidlem27  27752  mapdrn  32447
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-fo 5460
  Copyright terms: Public domain W3C validator