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

Theorem forn 5648
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 5452 . 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 4871    Fn wfn 5441   -onto->wfo 5444
This theorem is referenced by:  dffo2  5649  foima  5650  fodmrnu  5653  f1imacnv  5683  foimacnv  5684  foun  5685  resdif  5688  fococnv2  5693  fornex  5962  cbvfo  6014  isoini  6050  isofrlem  6052  isoselem  6053  wemoiso2  6071  f1opw2  6290  curry1  6430  curry2  6433  canth  6531  bren  7109  en1  7166  fopwdom  7208  domss2  7258  mapen  7263  ssenen  7273  phplem4  7281  php3  7285  ssfi  7321  fodomfib  7378  f1opwfi  7402  ordiso2  7476  ordtypelem10  7488  oismo  7501  brwdom  7527  brwdom2  7533  wdomtr  7535  unxpwdom2  7548  wemapwe  7646  infxpenc2lem1  7892  fseqen  7900  fodomfi2  7933  infpwfien  7935  infmap2  8090  ackbij2  8115  infpssr  8180  fodomb  8396  fpwwe2lem6  8502  fpwwe2lem9  8505  tskuni  8650  gruen  8679  hashfacen  11695  supcvg  12627  ruclem13  12833  unbenlem  13268  imasval  13729  imasaddfnlem  13745  imasvscafn  13754  imasless  13757  xpsfrn  13786  fulloppc  14111  imasmnd2  14724  imasgrp2  14925  oppglsm  15268  efgrelexlemb  15374  gsumzres  15509  gsumzcl  15510  gsumzf1o  15511  gsumzaddlem  15518  gsumconst  15524  gsumzmhm  15525  gsumzoppg  15531  dprdf1o  15582  imasrng  15717  gsumfsum  16758  zncyg  16821  znf1o  16824  znleval  16827  znunit  16836  cygznlem2a  16840  cmpfi  17463  cnconn  17477  1stcfb  17500  qtopval2  17720  basqtop  17735  tgqtop  17736  imastopn  17744  hmeontr  17793  hmeoqtop  17799  nrmhmph  17818  cmphaushmeo  17824  elfm3  17974  divstgpopn  18141  tsmsf1o  18166  imasf1oxmet  18397  imasf1omet  18398  imasf1oxms  18511  cnheiborlem  18971  ovolctb  19378  dyadmbl  19484  dvcnvrelem2  19894  dvcnvre  19895  efifo  20441  logrn  20448  dvrelog  20520  efopnlem2  20540  fsumdvdsmul  20972  eupares  21689  eupath2lem3  21693  isgrpo  21776  isgrpoi  21778  isgrp2d  21815  isgrpda  21877  rngopid  21903  opidon2  21904  circgrp  21954  rngmgmbs4  21997  pjrn  23201  ballotlemro  24772  erdsze2lem1  24881  cnpcon  24909  bdayrn  25624  axcontlem10  25904  mblfinlem  26234  volsupnfl  26241  ismtyres  26508  dnnumch2  27111  lnmlmic  27154  pwslnmlem1  27162  pwslnmlem2  27163  indlcim  27278  stoweidlem27  27743  mapdrn  32384
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 5452
  Copyright terms: Public domain W3C validator