Theorem forn 6750

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

Syntax hints:   → wi 4   = wceq 1542  ran crn 5626   Fn wfn 6488  –onto→wfo 6491

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 6499

This theorem is referenced by:  dffo2  6751  foima  6752  fodmrnu  6755  focnvimacdmdm  6759  focofo  6760  foco  6761  f1imacnv  6791  foimacnv  6792  foun  6793  resdif  6796  fococnv2  6801  foelcdmi  6896  f1ounsn  7221  cbvfo  7238  f1ocoima  7252  isoini  7287  isofrlem  7289  isoselem  7290  canth  7315  f1opw2  7616  focdmex  7903  wemoiso2  7921  curry1  8048  curry2  8051  mapfoss  8793  bren  8897  en1  8965  fopwdom  9017  domss2  9068  mapen  9073  ssenen  9083  ssfiALT  9102  phplem2  9133  php3  9137  fodomfib  9233  fodomfibOLD  9235  f1opwfi  9260  ordiso2  9424  ordtypelem10  9436  oismo  9449  brwdom  9476  brwdom2  9482  wdomtr  9484  unxpwdom2  9497  wemapwe  9612  infxpenc2lem1  9935  fseqen  9943  fodomfi2  9976  infpwfien  9978  infmap2  10133  ackbij2  10158  infpssr  10224  fodomb  10442  fpwwe2lem5  10552  fpwwe2lem8  10555  tskuni  10700  gruen  10729  supcvg  15815  ruclem13  16203  unbenlem  16873  imasval  17469  imasaddfnlem  17486  imasvscafn  17495  imasless  17498  xpsfrn  17526  fulloppc  17885  imasmnd2  18736  resgrpplusfrn  18920  imasgrp2  19025  oppglsm  19611  efgrelexlemb  19719  gsumzres  19878  gsumzcl2  19879  gsumzf1o  19881  gsumzaddlem  19890  gsumconst  19903  gsumzmhm  19906  gsumzoppg  19913  dprdf1o  20003  imasrng  20152  imasring  20304  gsumfsum  21427  zncyg  21541  znf1o  21544  znleval  21547  znunit  21556  cygznlem2a  21560  indlcim  21833  cmpfi  23386  cnconn  23400  1stcfb  23423  qtopval2  23674  basqtop  23689  tgqtop  23690  imastopn  23698  hmeontr  23747  hmeoqtop  23753  nrmhmph  23772  cmphaushmeo  23778  elfm3  23928  qustgpopn  24098  tsmsf1o  24123  imasf1oxmet  24353  imasf1omet  24354  imasf1oxms  24467  cnheiborlem  24934  ovolctb  25470  dyadmbl  25580  dvcnvrelem2  25998  dvcnvre  25999  efifo  26527  circgrp  26532  circsubm  26533  logrn  26538  dvrelog  26617  efopnlem2  26637  fsumdvdsmul  27175  bdayimaon  27674  noetasuplem4  27717  noetainflem4  27721  bdayrn  27760  noeta2  27770  negsunif  28064  negbdaylem  28065  zssno  28390  f1otrg  28956  axcontlem10  29059  isgrpo  30586  isgrpoi  30587  pjrn  31796  padct  32809  cycpmconjvlem  33220  cycpmconjslem2  33234  imaslmod  33431  esplysply  33733  qusdimsum  33791  sigapildsys  34325  carsgclctunlem3  34483  ballotlemro  34686  erdsze2lem1  35404  cnpconn  35431  poimirlem15  37973  mblfinlem2  37996  volsupnfl  38003  ismtyres  38146  rngopidOLD  38191  opidon2OLD  38192  rngmgmbs4  38269  isgrpda  38293  mapdrn  42112  ricdrng1  42990  dnnumch2  43494  lnmlmic  43537  pwslnmlem1  43541  pwslnmlem2  43542  ntrneifv2  44528  ssnnf1octb  45645  stoweidlem27  46476  fourierdlem51  46606  fourierdlem102  46657  fourierdlem114  46669  sge0fodjrnlem  46865  nnfoctbdjlem  46904  nnfoctbdj  46905  3f1oss1  47538  fonex  49357  tposres3  49371