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

Theorem forn 5597
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 5401 . 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 1649   ran crn 4820    Fn wfn 5390   -onto->wfo 5393
This theorem is referenced by:  dffo2  5598  foima  5599  fodmrnu  5602  f1imacnv  5632  foimacnv  5633  foun  5634  resdif  5637  fococnv2  5642  fornex  5910  cbvfo  5962  isoini  5998  isofrlem  6000  isoselem  6001  wemoiso2  6019  f1opw2  6238  curry1  6378  curry2  6381  canth  6476  bren  7054  en1  7111  fopwdom  7153  domss2  7203  mapen  7208  ssenen  7218  phplem4  7226  php3  7230  ssfi  7266  fodomfib  7323  f1opwfi  7346  ordiso2  7418  ordtypelem10  7430  oismo  7443  brwdom  7469  brwdom2  7475  wdomtr  7477  unxpwdom2  7490  wemapwe  7588  infxpenc2lem1  7834  fseqen  7842  fodomfi2  7875  infpwfien  7877  infmap2  8032  ackbij2  8057  infpssr  8122  fodomb  8338  fpwwe2lem6  8444  fpwwe2lem9  8447  tskuni  8592  gruen  8621  hashfacen  11631  supcvg  12563  ruclem13  12769  unbenlem  13204  imasval  13665  imasaddfnlem  13681  imasvscafn  13690  imasless  13693  xpsfrn  13722  fulloppc  14047  imasmnd2  14660  imasgrp2  14861  oppglsm  15204  efgrelexlemb  15310  gsumzres  15445  gsumzcl  15446  gsumzf1o  15447  gsumzaddlem  15454  gsumconst  15460  gsumzmhm  15461  gsumzoppg  15467  dprdf1o  15518  imasrng  15653  gsumfsum  16690  zncyg  16753  znf1o  16756  znleval  16759  znunit  16768  cygznlem2a  16772  cmpfi  17394  cnconn  17407  1stcfb  17430  qtopval2  17650  basqtop  17665  tgqtop  17666  imastopn  17674  hmeontr  17723  hmeoqtop  17729  nrmhmph  17748  cmphaushmeo  17754  elfm3  17904  divstgpopn  18071  tsmsf1o  18096  imasf1oxmet  18314  imasf1omet  18315  imasf1oxms  18410  cnheiborlem  18851  ovolctb  19254  dyadmbl  19360  dvcnvrelem2  19770  dvcnvre  19771  efifo  20317  logrn  20324  dvrelog  20396  efopnlem2  20416  fsumdvdsmul  20848  eupares  21546  eupath2lem3  21550  isgrpo  21633  isgrpoi  21635  isgrp2d  21672  isgrpda  21734  rngopid  21760  opidon2  21761  circgrp  21811  rngmgmbs4  21854  pjrn  23058  ballotlemro  24560  erdsze2lem1  24669  cnpcon  24697  bdayrn  25356  axcontlem10  25627  volsupnfl  25957  ismtyres  26209  dnnumch2  26812  lnmlmic  26856  pwslnmlem1  26864  pwslnmlem2  26865  indlcim  26980  stoweidlem27  27445  mapdrn  31765
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 5401
  Copyright terms: Public domain W3C validator