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

Theorem forn 5470
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 5277 . 2  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
21simprbi 450 1  |-  ( F : A -onto-> B  ->  ran  F  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   ran crn 4706    Fn wfn 5266   -onto->wfo 5269
This theorem is referenced by:  dffo2  5471  foima  5472  fodmrnu  5475  f1imacnv  5505  foimacnv  5506  foun  5507  resdif  5510  fococnv2  5515  fornex  5766  cbvfo  5815  isoini  5851  isofrlem  5853  isoselem  5854  wemoiso2  5872  f1opw2  6087  curry1  6226  curry2  6229  canth  6310  bren  6887  en1  6944  fopwdom  6986  domss2  7036  mapen  7041  ssenen  7051  phplem4  7059  php3  7063  ssfi  7099  fodomfib  7152  f1opwfi  7175  ordiso2  7246  ordtypelem10  7258  oismo  7271  brwdom  7297  brwdom2  7303  wdomtr  7305  unxpwdom2  7318  wemapwe  7416  infxpenc2lem1  7662  fseqen  7670  fodomfi2  7703  infpwfien  7705  infmap2  7860  ackbij2  7885  infpssr  7950  fodomb  8167  fpwwe2lem6  8273  fpwwe2lem9  8276  tskuni  8421  gruen  8450  hashfacen  11408  supcvg  12330  ruclem13  12536  unbenlem  12971  imasval  13430  imasaddfnlem  13446  imasvscafn  13455  imasless  13458  xpsfrn  13487  fulloppc  13812  imasmnd2  14425  imasgrp2  14626  oppglsm  14969  efgrelexlemb  15075  gsumzres  15210  gsumzcl  15211  gsumzf1o  15212  gsumzaddlem  15219  gsumconst  15225  gsumzmhm  15226  gsumzoppg  15232  dprdf1o  15283  imasrng  15418  gsumfsum  16455  zncyg  16518  znf1o  16521  znleval  16524  znunit  16533  cygznlem2a  16537  cmpfi  17151  cnconn  17164  1stcfb  17187  qtopval2  17403  basqtop  17418  tgqtop  17419  imastopn  17427  hmeontr  17476  hmeoqtop  17482  nrmhmph  17501  cmphaushmeo  17507  elfm3  17661  divstgpopn  17818  tsmsf1o  17843  imasf1oxmet  17955  imasf1omet  17956  imasf1oxms  18051  cnheiborlem  18468  ovolctb  18865  dyadmbl  18971  dvcnvrelem2  19381  dvcnvre  19382  efifo  19925  logrn  19932  dvrelog  20000  efopnlem2  20020  fsumdvdsmul  20451  isgrpo  20879  isgrpoi  20881  isgrp2d  20918  isgrpda  20980  rngopid  21006  opidon2  21007  circgrp  21057  rngmgmbs4  21100  pjrn  22302  ballotlemro  23097  erdsze2lem1  23749  cnpcon  23776  eupares  23914  eupath2lem3  23918  bdayrn  24402  axcontlem10  24673  domrancur1b  25303  domrancur1c  25305  rngapm  25473  zintdom  25541  tcnvec  25793  ismtyres  26635  dnnumch2  27245  lnmlmic  27289  pwslnmlem1  27297  pwslnmlem2  27298  indlcim  27413  stoweidlem27  27879  mapdrn  32461
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 177  df-an 360  df-fo 5277
  Copyright terms: Public domain W3C validator