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

Theorem forn 5454
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 5261 . 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 1623   ran crn 4690    Fn wfn 5250   -onto->wfo 5253
This theorem is referenced by:  dffo2  5455  foima  5456  fodmrnu  5459  f1imacnv  5489  foimacnv  5490  foun  5491  resdif  5494  fococnv2  5499  fornex  5750  cbvfo  5799  isoini  5835  isofrlem  5837  isoselem  5838  wemoiso2  5856  f1opw2  6071  curry1  6210  curry2  6213  canth  6294  bren  6871  en1  6928  fopwdom  6970  domss2  7020  mapen  7025  ssenen  7035  phplem4  7043  php3  7047  ssfi  7083  fodomfib  7136  f1opwfi  7159  ordiso2  7230  ordtypelem10  7242  oismo  7255  brwdom  7281  brwdom2  7287  wdomtr  7289  unxpwdom2  7302  wemapwe  7400  infxpenc2lem1  7646  fseqen  7654  fodomfi2  7687  infpwfien  7689  infmap2  7844  ackbij2  7869  infpssr  7934  fodomb  8151  fpwwe2lem6  8257  fpwwe2lem9  8260  tskuni  8405  gruen  8434  hashfacen  11392  supcvg  12314  ruclem13  12520  unbenlem  12955  imasval  13414  imasaddfnlem  13430  imasvscafn  13439  imasless  13442  xpsfrn  13471  fulloppc  13796  imasmnd2  14409  imasgrp2  14610  oppglsm  14953  efgrelexlemb  15059  gsumzres  15194  gsumzcl  15195  gsumzf1o  15196  gsumzaddlem  15203  gsumconst  15209  gsumzmhm  15210  gsumzoppg  15216  dprdf1o  15267  imasrng  15402  gsumfsum  16439  zncyg  16502  znf1o  16505  znleval  16508  znunit  16517  cygznlem2a  16521  cmpfi  17135  cnconn  17148  1stcfb  17171  qtopval2  17387  basqtop  17402  tgqtop  17403  imastopn  17411  hmeontr  17460  hmeoqtop  17466  nrmhmph  17485  cmphaushmeo  17491  elfm3  17645  divstgpopn  17802  tsmsf1o  17827  imasf1oxmet  17939  imasf1omet  17940  imasf1oxms  18035  cnheiborlem  18452  ovolctb  18849  dyadmbl  18955  dvcnvrelem2  19365  dvcnvre  19366  efifo  19909  logrn  19916  dvrelog  19984  efopnlem2  20004  fsumdvdsmul  20435  isgrpo  20863  isgrpoi  20865  isgrp2d  20902  isgrpda  20964  rngopid  20990  opidon2  20991  circgrp  21041  rngmgmbs4  21084  pjrn  22286  ballotlemro  23081  erdsze2lem1  23734  cnpcon  23761  eupares  23899  eupath2lem3  23903  bdayrn  24331  axcontlem10  24601  domrancur1b  25200  domrancur1c  25202  rngapm  25370  zintdom  25438  tcnvec  25690  ismtyres  26532  dnnumch2  27142  lnmlmic  27186  pwslnmlem1  27194  pwslnmlem2  27195  indlcim  27310  stoweidlem27  27776  mapdrn  31839
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 5261
  Copyright terms: Public domain W3C validator