Theorem forn 6755

Description: The codomain of an onto function is its range. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
forn	⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)

Proof of Theorem forn

Step	Hyp	Ref	Expression
1		df-fo 6504	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
2	1	simprbi 497	1 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)

Syntax hints:   → wi 4   = wceq 1542  ran crn 5632   Fn wfn 6493  –onto→wfo 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-fo 6504

This theorem is referenced by:  dffo2  6756  foima  6757  fodmrnu  6760  focnvimacdmdm  6764  focofo  6765  foco  6766  f1imacnv  6796  foimacnv  6797  foun  6798  resdif  6801  fococnv2  6806  foelcdmi  6901  f1ounsn  7227  cbvfo  7244  f1ocoima  7258  isoini  7293  isofrlem  7295  isoselem  7296  canth  7321  f1opw2  7622  focdmex  7909  wemoiso2  7927  curry1  8054  curry2  8057  mapfoss  8799  bren  8903  en1  8971  fopwdom  9023  domss2  9074  mapen  9079  ssenen  9089  ssfiALT  9108  phplem2  9139  php3  9143  fodomfib  9239  fodomfibOLD  9241  f1opwfi  9266  ordiso2  9430  ordtypelem10  9442  oismo  9455  brwdom  9482  brwdom2  9488  wdomtr  9490  unxpwdom2  9503  wemapwe  9618  infxpenc2lem1  9941  fseqen  9949  fodomfi2  9982  infpwfien  9984  infmap2  10139  ackbij2  10164  infpssr  10230  fodomb  10448  fpwwe2lem5  10558  fpwwe2lem8  10561  tskuni  10706  gruen  10735  supcvg  15821  ruclem13  16209  unbenlem  16879  imasval  17475  imasaddfnlem  17492  imasvscafn  17501  imasless  17504  xpsfrn  17532  fulloppc  17891  imasmnd2  18742  resgrpplusfrn  18926  imasgrp2  19031  oppglsm  19617  efgrelexlemb  19725  gsumzres  19884  gsumzcl2  19885  gsumzf1o  19887  gsumzaddlem  19896  gsumconst  19909  gsumzmhm  19912  gsumzoppg  19919  dprdf1o  20009  imasrng  20158  imasring  20310  gsumfsum  21414  zncyg  21528  znf1o  21531  znleval  21534  znunit  21543  cygznlem2a  21547  indlcim  21820  cmpfi  23373  cnconn  23387  1stcfb  23410  qtopval2  23661  basqtop  23676  tgqtop  23677  imastopn  23685  hmeontr  23734  hmeoqtop  23740  nrmhmph  23759  cmphaushmeo  23765  elfm3  23915  qustgpopn  24085  tsmsf1o  24110  imasf1oxmet  24340  imasf1omet  24341  imasf1oxms  24454  cnheiborlem  24921  ovolctb  25457  dyadmbl  25567  dvcnvrelem2  25985  dvcnvre  25986  efifo  26511  circgrp  26516  circsubm  26517  logrn  26522  dvrelog  26601  efopnlem2  26621  fsumdvdsmul  27158  bdayimaon  27657  noetasuplem4  27700  noetainflem4  27704  bdayrn  27743  noeta2  27753  negsunif  28047  negbdaylem  28048  zssno  28373  f1otrg  28939  axcontlem10  29042  isgrpo  30568  isgrpoi  30569  pjrn  31778  padct  32791  cycpmconjvlem  33202  cycpmconjslem2  33216  imaslmod  33413  esplysply  33715  qusdimsum  33772  sigapildsys  34306  carsgclctunlem3  34464  ballotlemro  34667  erdsze2lem1  35385  cnpconn  35412  poimirlem15  37956  mblfinlem2  37979  volsupnfl  37986  ismtyres  38129  rngopidOLD  38174  opidon2OLD  38175  rngmgmbs4  38252  isgrpda  38276  mapdrn  42095  ricdrng1  42973  dnnumch2  43473  lnmlmic  43516  pwslnmlem1  43520  pwslnmlem2  43521  ntrneifv2  44507  ssnnf1octb  45624  stoweidlem27  46455  fourierdlem51  46585  fourierdlem102  46636  fourierdlem114  46648  sge0fodjrnlem  46844  nnfoctbdjlem  46883  nnfoctbdj  46884  3f1oss1  47523  fonex  49342  tposres3  49356