Theorem forn 6738

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

Syntax hints:   → wi 4   = wceq 1541  ran crn 5615   Fn wfn 6476  –onto→wfo 6479

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 6487

This theorem is referenced by:  dffo2  6739  foima  6740  fodmrnu  6743  focnvimacdmdm  6747  focofo  6748  foco  6749  f1imacnv  6779  foimacnv  6780  foun  6781  resdif  6784  fococnv2  6789  foelcdmi  6883  f1ounsn  7206  cbvfo  7223  f1ocoima  7237  isoini  7272  isofrlem  7274  isoselem  7275  canth  7300  f1opw2  7601  focdmex  7888  wemoiso2  7906  curry1  8034  curry2  8037  mapfoss  8776  bren  8879  en1  8946  fopwdom  8998  domss2  9049  mapen  9054  ssenen  9064  ssfiALT  9083  phplem2  9114  php3  9118  fodomfib  9213  fodomfibOLD  9215  f1opwfi  9240  ordiso2  9401  ordtypelem10  9413  oismo  9426  brwdom  9453  brwdom2  9459  wdomtr  9461  unxpwdom2  9474  wemapwe  9587  infxpenc2lem1  9910  fseqen  9918  fodomfi2  9951  infpwfien  9953  infmap2  10108  ackbij2  10133  infpssr  10199  fodomb  10417  fpwwe2lem5  10526  fpwwe2lem8  10529  tskuni  10674  gruen  10703  supcvg  15763  ruclem13  16151  unbenlem  16820  imasval  17415  imasaddfnlem  17432  imasvscafn  17441  imasless  17444  xpsfrn  17472  fulloppc  17831  imasmnd2  18682  resgrpplusfrn  18863  imasgrp2  18968  oppglsm  19554  efgrelexlemb  19662  gsumzres  19821  gsumzcl2  19822  gsumzf1o  19824  gsumzaddlem  19833  gsumconst  19846  gsumzmhm  19849  gsumzoppg  19856  dprdf1o  19946  imasrng  20095  imasring  20248  gsumfsum  21371  zncyg  21485  znf1o  21488  znleval  21491  znunit  21500  cygznlem2a  21504  indlcim  21777  cmpfi  23323  cnconn  23337  1stcfb  23360  qtopval2  23611  basqtop  23626  tgqtop  23627  imastopn  23635  hmeontr  23684  hmeoqtop  23690  nrmhmph  23709  cmphaushmeo  23715  elfm3  23865  qustgpopn  24035  tsmsf1o  24060  imasf1oxmet  24290  imasf1omet  24291  imasf1oxms  24404  cnheiborlem  24880  ovolctb  25418  dyadmbl  25528  dvcnvrelem2  25950  dvcnvre  25951  efifo  26483  circgrp  26488  circsubm  26489  logrn  26494  dvrelog  26573  efopnlem2  26593  fsumdvdsmul  27132  fsumdvdsmulOLD  27134  bdayimaon  27632  noetasuplem4  27675  noetainflem4  27679  bdayrn  27714  noeta2  27724  negsunif  27997  negsbdaylem  27998  zssno  28305  f1otrg  28849  axcontlem10  28951  isgrpo  30477  isgrpoi  30478  pjrn  31687  padct  32701  cycpmconjvlem  33110  cycpmconjslem2  33124  imaslmod  33318  esplysply  33592  qusdimsum  33641  sigapildsys  34175  carsgclctunlem3  34333  ballotlemro  34536  erdsze2lem1  35247  cnpconn  35274  poimirlem15  37683  mblfinlem2  37706  volsupnfl  37713  ismtyres  37856  rngopidOLD  37901  opidon2OLD  37902  rngmgmbs4  37979  isgrpda  38003  mapdrn  41696  ricdrng1  42569  dnnumch2  43086  lnmlmic  43129  pwslnmlem1  43133  pwslnmlem2  43134  ntrneifv2  44121  ssnnf1octb  45239  stoweidlem27  46073  fourierdlem51  46203  fourierdlem102  46254  fourierdlem114  46266  sge0fodjrnlem  46462  nnfoctbdjlem  46501  nnfoctbdj  46502  3f1oss1  47114  fonex  48906  tposres3  48920