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  17866  imasmnd2  18683  resgrpplusfrn  18864  imasgrp2  18969  oppglsm  19556  efgrelexlemb  19664  gsumzres  19823  gsumzcl2  19824  gsumzf1o  19826  gsumzaddlem  19835  gsumconst  19848  gsumzmhm  19851  gsumzoppg  19858  dprdf1o  19948  imasrng  20097  imasring  20250  gsumfsum  21376  zncyg  21490  znf1o  21493  znleval  21496  znunit  21505  cygznlem2a  21509  indlcim  21782  cmpfi  23328  cnconn  23342  1stcfb  23365  qtopval2  23616  basqtop  23631  tgqtop  23632  imastopn  23640  hmeontr  23689  hmeoqtop  23695  nrmhmph  23714  cmphaushmeo  23720  elfm3  23870  qustgpopn  24040  tsmsf1o  24065  imasf1oxmet  24296  imasf1omet  24297  imasf1oxms  24410  cnheiborlem  24886  ovolctb  25424  dyadmbl  25534  dvcnvrelem2  25956  dvcnvre  25957  efifo  26489  circgrp  26494  circsubm  26495  logrn  26500  dvrelog  26579  efopnlem2  26599  fsumdvdsmul  27138  fsumdvdsmulOLD  27140  bdayimaon  27638  noetasuplem4  27681  noetainflem4  27685  bdayrn  27720  noeta2  27730  negsunif  28001  negsbdaylem  28002  zssno  28309  f1otrg  28851  axcontlem10  28953  isgrpo  30476  isgrpoi  30477  pjrn  31686  padct  32693  cycpmconjvlem  33113  cycpmconjslem2  33127  imaslmod  33317  qusdimsum  33617  sigapildsys  34145  carsgclctunlem3  34304  ballotlemro  34507  erdsze2lem1  35183  cnpconn  35210  poimirlem15  37622  mblfinlem2  37645  volsupnfl  37652  ismtyres  37795  rngopidOLD  37840  opidon2OLD  37841  rngmgmbs4  37918  isgrpda  37942  mapdrn  41636  ricdrng1  42509  dnnumch2  43027  lnmlmic  43070  pwslnmlem1  43074  pwslnmlem2  43075  ntrneifv2  44062  ssnnf1octb  45181  stoweidlem27  46018  fourierdlem51  46148  fourierdlem102  46199  fourierdlem114  46211  sge0fodjrnlem  46407  nnfoctbdjlem  46446  nnfoctbdj  46447  3f1oss1  47069  fonex  48848  tposres3  48862