Theorem forn 6749

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

Syntax hints:   → wi 4   = wceq 1541  ran crn 5625   Fn wfn 6487  –onto→wfo 6490

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 6498

This theorem is referenced by:  dffo2  6750  foima  6751  fodmrnu  6754  focnvimacdmdm  6758  focofo  6759  foco  6760  f1imacnv  6790  foimacnv  6791  foun  6792  resdif  6795  fococnv2  6800  foelcdmi  6895  f1ounsn  7218  cbvfo  7235  f1ocoima  7249  isoini  7284  isofrlem  7286  isoselem  7287  canth  7312  f1opw2  7613  focdmex  7900  wemoiso2  7918  curry1  8046  curry2  8049  mapfoss  8789  bren  8893  en1  8961  fopwdom  9013  domss2  9064  mapen  9069  ssenen  9079  ssfiALT  9098  phplem2  9129  php3  9133  fodomfib  9229  fodomfibOLD  9231  f1opwfi  9256  ordiso2  9420  ordtypelem10  9432  oismo  9445  brwdom  9472  brwdom2  9478  wdomtr  9480  unxpwdom2  9493  wemapwe  9606  infxpenc2lem1  9929  fseqen  9937  fodomfi2  9970  infpwfien  9972  infmap2  10127  ackbij2  10152  infpssr  10218  fodomb  10436  fpwwe2lem5  10546  fpwwe2lem8  10549  tskuni  10694  gruen  10723  supcvg  15779  ruclem13  16167  unbenlem  16836  imasval  17432  imasaddfnlem  17449  imasvscafn  17458  imasless  17461  xpsfrn  17489  fulloppc  17848  imasmnd2  18699  resgrpplusfrn  18880  imasgrp2  18985  oppglsm  19571  efgrelexlemb  19679  gsumzres  19838  gsumzcl2  19839  gsumzf1o  19841  gsumzaddlem  19850  gsumconst  19863  gsumzmhm  19866  gsumzoppg  19873  dprdf1o  19963  imasrng  20112  imasring  20266  gsumfsum  21389  zncyg  21503  znf1o  21506  znleval  21509  znunit  21518  cygznlem2a  21522  indlcim  21795  cmpfi  23352  cnconn  23366  1stcfb  23389  qtopval2  23640  basqtop  23655  tgqtop  23656  imastopn  23664  hmeontr  23713  hmeoqtop  23719  nrmhmph  23738  cmphaushmeo  23744  elfm3  23894  qustgpopn  24064  tsmsf1o  24089  imasf1oxmet  24319  imasf1omet  24320  imasf1oxms  24433  cnheiborlem  24909  ovolctb  25447  dyadmbl  25557  dvcnvrelem2  25979  dvcnvre  25980  efifo  26512  circgrp  26517  circsubm  26518  logrn  26523  dvrelog  26602  efopnlem2  26622  fsumdvdsmul  27161  fsumdvdsmulOLD  27163  bdayimaon  27661  noetasuplem4  27704  noetainflem4  27708  bdayrn  27747  noeta2  27757  negsunif  28051  negbdaylem  28052  zssno  28377  f1otrg  28943  axcontlem10  29046  isgrpo  30572  isgrpoi  30573  pjrn  31782  padct  32797  cycpmconjvlem  33223  cycpmconjslem2  33237  imaslmod  33434  esplysply  33729  qusdimsum  33785  sigapildsys  34319  carsgclctunlem3  34477  ballotlemro  34680  erdsze2lem1  35397  cnpconn  35424  poimirlem15  37836  mblfinlem2  37859  volsupnfl  37866  ismtyres  38009  rngopidOLD  38054  opidon2OLD  38055  rngmgmbs4  38132  isgrpda  38156  mapdrn  41909  ricdrng1  42783  dnnumch2  43287  lnmlmic  43330  pwslnmlem1  43334  pwslnmlem2  43335  ntrneifv2  44321  ssnnf1octb  45438  stoweidlem27  46271  fourierdlem51  46401  fourierdlem102  46452  fourierdlem114  46464  sge0fodjrnlem  46660  nnfoctbdjlem  46699  nnfoctbdj  46700  3f1oss1  47321  fonex  49112  tposres3  49126