Theorem forn 6757

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

Syntax hints:   → wi 4   = wceq 1540  ran crn 5632   Fn wfn 6494  –onto→wfo 6497

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 6505

This theorem is referenced by:  dffo2  6758  foima  6759  fodmrnu  6762  focnvimacdmdm  6766  focofo  6767  foco  6768  f1imacnv  6798  foimacnv  6799  foun  6800  resdif  6803  fococnv2  6808  foelcdmi  6904  f1ounsn  7229  cbvfo  7246  f1ocoima  7260  isoini  7295  isofrlem  7297  isoselem  7298  canth  7323  f1opw2  7624  focdmex  7914  wemoiso2  7932  curry1  8060  curry2  8063  mapfoss  8802  bren  8905  en1  8972  fopwdom  9026  domss2  9077  mapen  9082  ssenen  9092  ssfiALT  9115  phplem2  9146  php3  9150  fodomfib  9256  fodomfibOLD  9258  f1opwfi  9283  ordiso2  9444  ordtypelem10  9456  oismo  9469  brwdom  9496  brwdom2  9502  wdomtr  9504  unxpwdom2  9517  wemapwe  9626  infxpenc2lem1  9948  fseqen  9956  fodomfi2  9989  infpwfien  9991  infmap2  10146  ackbij2  10171  infpssr  10237  fodomb  10455  fpwwe2lem5  10564  fpwwe2lem8  10567  tskuni  10712  gruen  10741  supcvg  15798  ruclem13  16186  unbenlem  16855  imasval  17450  imasaddfnlem  17467  imasvscafn  17476  imasless  17479  xpsfrn  17507  fulloppc  17862  imasmnd2  18677  resgrpplusfrn  18858  imasgrp2  18963  oppglsm  19548  efgrelexlemb  19656  gsumzres  19815  gsumzcl2  19816  gsumzf1o  19818  gsumzaddlem  19827  gsumconst  19840  gsumzmhm  19843  gsumzoppg  19850  dprdf1o  19940  imasrng  20062  imasring  20215  gsumfsum  21327  zncyg  21434  znf1o  21437  znleval  21440  znunit  21449  cygznlem2a  21453  indlcim  21725  cmpfi  23271  cnconn  23285  1stcfb  23308  qtopval2  23559  basqtop  23574  tgqtop  23575  imastopn  23583  hmeontr  23632  hmeoqtop  23638  nrmhmph  23657  cmphaushmeo  23663  elfm3  23813  qustgpopn  23983  tsmsf1o  24008  imasf1oxmet  24239  imasf1omet  24240  imasf1oxms  24353  cnheiborlem  24829  ovolctb  25367  dyadmbl  25477  dvcnvrelem2  25899  dvcnvre  25900  efifo  26432  circgrp  26437  circsubm  26438  logrn  26443  dvrelog  26522  efopnlem2  26542  fsumdvdsmul  27081  fsumdvdsmulOLD  27083  bdayimaon  27581  noetasuplem4  27624  noetainflem4  27628  bdayrn  27663  noeta2  27672  negsunif  27937  negsbdaylem  27938  zssno  28245  f1otrg  28774  axcontlem10  28876  isgrpo  30399  isgrpoi  30400  pjrn  31609  padct  32616  cycpmconjvlem  33071  cycpmconjslem2  33085  imaslmod  33297  qusdimsum  33597  sigapildsys  34125  carsgclctunlem3  34284  ballotlemro  34487  erdsze2lem1  35163  cnpconn  35190  poimirlem15  37602  mblfinlem2  37625  volsupnfl  37632  ismtyres  37775  rngopidOLD  37820  opidon2OLD  37821  rngmgmbs4  37898  isgrpda  37922  mapdrn  41616  ricdrng1  42489  dnnumch2  43007  lnmlmic  43050  pwslnmlem1  43054  pwslnmlem2  43055  ntrneifv2  44042  ssnnf1octb  45161  stoweidlem27  45998  fourierdlem51  46128  fourierdlem102  46179  fourierdlem114  46191  sge0fodjrnlem  46387  nnfoctbdjlem  46426  nnfoctbdj  46427  3f1oss1  47049  fonex  48828  tposres3  48842