Theorem forn 6742

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

Syntax hints:   → wi 4   = wceq 1547  ran crn 5619   Fn wfn 6480  –onto→wfo 6483

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 208  df-an 397  df-fo 6491

This theorem is referenced by:  dffo2  6743  foima  6744  fodmrnu  6747  focnvimacdmdm  6751  focofo  6752  foco  6753  f1imacnv  6783  foimacnv  6784  foun  6785  resdif  6788  fococnv2  6793  foelcdmi  6888  f1ounsn  7216  cbvfo  7233  f1ocoima  7247  isoini  7282  isofrlem  7284  isoselem  7285  canth  7310  f1opw2  7611  focdmex  7898  wemoiso2  7916  curry1  8043  curry2  8046  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  9609  infxpenc2lem1  9932  fseqen  9940  fodomfi2  9973  infpwfien  9975  infmap2  10130  ackbij2  10155  infpssr  10221  fodomb  10439  fpwwe2lem5  10549  fpwwe2lem8  10552  tskuni  10697  gruen  10726  supcvg  15812  ruclem13  16200  unbenlem  16870  imasval  17466  imasaddfnlem  17483  imasvscafn  17492  imasless  17495  xpsfrn  17523  fulloppc  17882  imasmnd2  18733  resgrpplusfrn  18917  imasgrp2  19022  oppglsm  19608  efgrelexlemb  19716  gsumzres  19875  gsumzcl2  19876  gsumzf1o  19878  gsumzaddlem  19887  gsumconst  19900  gsumzmhm  19903  gsumzoppg  19910  dprdf1o  20000  imasrng  20149  imasring  20301  gsumfsum  21409  zncyg  21523  znf1o  21526  znleval  21529  znunit  21538  cygznlem2a  21542  indlcim  21815  cmpfi  23391  cnconn  23405  1stcfb  23428  qtopval2  23679  basqtop  23694  tgqtop  23695  imastopn  23703  hmeontr  23752  hmeoqtop  23758  nrmhmph  23777  cmphaushmeo  23783  elfm3  23933  qustgpopn  24103  tsmsf1o  24128  imasf1oxmet  24358  imasf1omet  24359  imasf1oxms  24472  cnheiborlem  24939  ovolctb  25475  dyadmbl  25585  dvcnvrelem2  26003  dvcnvre  26004  efifo  26529  circgrp  26534  circsubm  26535  logrn  26540  dvrelog  26619  efopnlem2  26639  fsumdvdsmul  27176  bdayimaon  27675  noetasuplem4  27718  noetainflem4  27722  bdayrn  27761  noeta2  27771  negsunif  28065  negbdaylem  28066  zssno  28391  f1otrg  28957  axcontlem10  29060  isgrpo  30586  isgrpoi  30587  pjrn  31796  padct  32810  cycpmconjvlem  33222  cycpmconjslem2  33236  imaslmod  33436  esplysply  33755  qusdimsum  33812  sigapildsys  34346  carsgclctunlem3  34504  ballotlemro  34707  erdsze2lem1  35431  cnpconn  35458  poimirlem15  38002  mblfinlem2  38025  volsupnfl  38032  ismtyres  38175  rngopidOLD  38220  opidon2OLD  38221  rngmgmbs4  38298  isgrpda  38322  mapdrn  42141  ricdrng1  43014  dnnumch2  43490  lnmlmic  43533  pwslnmlem1  43537  pwslnmlem2  43538  ntrneifv2  44524  ssnnf1octb  45641  stoweidlem27  46470  fourierdlem51  46600  fourierdlem102  46651  fourierdlem114  46663  sge0fodjrnlem  46859  nnfoctbdjlem  46898  nnfoctbdj  46899  3f1oss1  47538  fonex  49357  tposres3  49371