Theorem forn 6793

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 6537	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
2	1	simprbi 496	1 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)

Syntax hints:   → wi 4   = wceq 1540  ran crn 5655   Fn wfn 6526  –onto→wfo 6529

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 6537

This theorem is referenced by:  dffo2  6794  foima  6795  fodmrnu  6798  focnvimacdmdm  6802  focofo  6803  foco  6804  f1imacnv  6834  foimacnv  6835  foun  6836  resdif  6839  fococnv2  6844  foelcdmi  6940  f1ounsn  7265  cbvfo  7282  f1ocoima  7296  isoini  7331  isofrlem  7333  isoselem  7334  canth  7359  f1opw2  7662  focdmex  7954  wemoiso2  7973  curry1  8103  curry2  8106  mapfoss  8866  bren  8969  en1  9038  fopwdom  9094  domss2  9150  mapen  9155  ssenen  9165  ssfiALT  9188  phplem2  9219  php3  9223  php3OLD  9233  fodomfib  9341  fodomfibOLD  9343  f1opwfi  9368  ordiso2  9529  ordtypelem10  9541  oismo  9554  brwdom  9581  brwdom2  9587  wdomtr  9589  unxpwdom2  9602  wemapwe  9711  infxpenc2lem1  10033  fseqen  10041  fodomfi2  10074  infpwfien  10076  infmap2  10231  ackbij2  10256  infpssr  10322  fodomb  10540  fpwwe2lem5  10649  fpwwe2lem8  10652  tskuni  10797  gruen  10826  supcvg  15872  ruclem13  16260  unbenlem  16928  imasval  17525  imasaddfnlem  17542  imasvscafn  17551  imasless  17554  xpsfrn  17582  fulloppc  17937  imasmnd2  18752  resgrpplusfrn  18933  imasgrp2  19038  oppglsm  19623  efgrelexlemb  19731  gsumzres  19890  gsumzcl2  19891  gsumzf1o  19893  gsumzaddlem  19902  gsumconst  19915  gsumzmhm  19918  gsumzoppg  19925  dprdf1o  20015  imasrng  20137  imasring  20290  gsumfsum  21402  zncyg  21509  znf1o  21512  znleval  21515  znunit  21524  cygznlem2a  21528  indlcim  21800  cmpfi  23346  cnconn  23360  1stcfb  23383  qtopval2  23634  basqtop  23649  tgqtop  23650  imastopn  23658  hmeontr  23707  hmeoqtop  23713  nrmhmph  23732  cmphaushmeo  23738  elfm3  23888  qustgpopn  24058  tsmsf1o  24083  imasf1oxmet  24314  imasf1omet  24315  imasf1oxms  24428  cnheiborlem  24904  ovolctb  25443  dyadmbl  25553  dvcnvrelem2  25975  dvcnvre  25976  efifo  26508  circgrp  26513  circsubm  26514  logrn  26519  dvrelog  26598  efopnlem2  26618  fsumdvdsmul  27157  fsumdvdsmulOLD  27159  bdayimaon  27657  noetasuplem4  27700  noetainflem4  27704  bdayrn  27739  noeta2  27748  negsunif  28013  negsbdaylem  28014  zssno  28321  f1otrg  28850  axcontlem10  28952  isgrpo  30478  isgrpoi  30479  pjrn  31688  padct  32697  cycpmconjvlem  33152  cycpmconjslem2  33166  imaslmod  33368  qusdimsum  33668  sigapildsys  34193  carsgclctunlem3  34352  ballotlemro  34555  erdsze2lem1  35225  cnpconn  35252  poimirlem15  37659  mblfinlem2  37682  volsupnfl  37689  ismtyres  37832  rngopidOLD  37877  opidon2OLD  37878  rngmgmbs4  37955  isgrpda  37979  mapdrn  41668  ricdrng1  42551  dnnumch2  43069  lnmlmic  43112  pwslnmlem1  43116  pwslnmlem2  43117  ntrneifv2  44104  ssnnf1octb  45218  stoweidlem27  46056  fourierdlem51  46186  fourierdlem102  46237  fourierdlem114  46249  sge0fodjrnlem  46445  nnfoctbdjlem  46484  nnfoctbdj  46485  3f1oss1  47104  fonex  48842  tposres3  48856