Theorem forn 6781

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

Syntax hints:   → wi 4   = wceq 1560  ran crn 5648   Fn wfn 6516  –onto→wfo 6519

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 209  df-an 400  df-fo 6527

This theorem is referenced by:  dffo2  6782  foima  6783  fodmrnu  6786  focnvimacdmdm  6790  focofo  6791  foco  6792  f1imacnv  6823  foimacnv  6824  foun  6825  resdif  6828  fococnv2  6833  foelcdmi  6928  f1ounsn  7256  cbvfo  7273  f1ocoima  7287  isoini  7322  isofrlem  7324  isoselem  7325  canth  7350  f1opw2  7651  focdmex  7937  wemoiso2  7955  curry1  8083  curry2  8086  mapfoss  8833  bren  8937  en1  9005  fopwdom  9057  domss2  9108  mapen  9113  ssenen  9123  ssfiALT  9142  phplem2  9173  php3  9177  fodomfib  9273  fodomfibOLD  9274  f1opwfi  9299  ordiso2  9463  ordtypelem10  9475  oismo  9488  brwdom  9515  brwdom2  9521  wdomtr  9523  unxpwdom2  9536  wemapwe  9652  infxpenc2lem1  9975  fseqen  9983  fodomfi2  10016  infpwfien  10018  infmap2  10173  ackbij2  10198  infpssr  10265  fodomb  10483  fpwwe2lem5  10593  fpwwe2lem8  10596  tskuni  10741  gruen  10770  supcvg  15886  ruclem13  16274  unbenlem  16944  imasval  17541  imasaddfnlem  17558  imasvscafn  17567  imasless  17570  xpsfrn  17598  fulloppc  17957  imasmnd2  18808  resgrpplusfrn  18992  imasgrp2  19097  oppglsm  19682  efgrelexlemb  19790  gsumzres  19949  gsumzcl2  19950  gsumzf1o  19952  gsumzaddlem  19961  gsumconst  19974  gsumzmhm  19977  gsumzoppg  19984  dprdf1o  20074  imasrng  20223  imasring  20375  gsumfsum  21483  zncyg  21597  znf1o  21600  znleval  21603  znunit  21612  cygznlem2a  21616  indlcim  21889  cmpfi  23465  cnconn  23479  1stcfb  23502  qtopval2  23753  basqtop  23768  tgqtop  23769  imastopn  23777  hmeontr  23826  hmeoqtop  23832  nrmhmph  23851  cmphaushmeo  23857  elfm3  24007  qustgpopn  24177  tsmsf1o  24202  imasf1oxmet  24432  imasf1omet  24433  imasf1oxms  24546  cnheiborlem  25013  ovolctb  25549  dyadmbl  25659  dvcnvrelem2  26077  dvcnvre  26078  efifo  26609  circgrp  26614  circsubm  26615  logrn  26620  dvrelog  26699  efopnlem2  26719  fsumdvdsmul  27256  bdayimaon  27754  noetasuplem4  27797  noetainflem4  27801  bdayrn  27841  noeta2  27851  negsunif  28145  negbdaylem  28146  zssno  28471  f1otrg  29068  axcontlem10  29171  isgrpo  30697  isgrpoi  30698  pjrn  31907  padct  32917  cycpmconjvlem  33318  cycpmconjslem2  33332  imaslmod  33536  esplysply  33865  qusdimsum  33922  sigapildsys  34456  carsgclctunlem3  34614  ballotlemro  34817  onvfowev  35456  erdsze2lem1  35550  cnpconn  35577  poimirlem15  38131  mblfinlem2  38154  volsupnfl  38161  ismtyres  38304  rngopidOLD  38349  opidon2OLD  38350  rngmgmbs4  38427  isgrpda  38451  mapdrn  42270  ricdrng1  43143  dnnumch2  43619  lnmlmic  43662  pwslnmlem1  43666  pwslnmlem2  43667  ntrneifv2  44653  ssnnf1octb  45769  stoweidlem27  46598  fourierdlem51  46728  fourierdlem102  46779  fourierdlem114  46791  sge0fodjrnlem  46987  nnfoctbdjlem  47026  nnfoctbdj  47027  3f1oss1  47666  fonex  49485  tposres3  49499