Theorem forn 6739

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

Syntax hints:   → wi 4   = wceq 1540  ran crn 5620   Fn wfn 6477  –onto→wfo 6480

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 6488

This theorem is referenced by:  dffo2  6740  foima  6741  fodmrnu  6744  focnvimacdmdm  6748  focofo  6749  foco  6750  f1imacnv  6780  foimacnv  6781  foun  6782  resdif  6785  fococnv2  6790  foelcdmi  6884  f1ounsn  7209  cbvfo  7226  f1ocoima  7240  isoini  7275  isofrlem  7277  isoselem  7278  canth  7303  f1opw2  7604  focdmex  7891  wemoiso2  7909  curry1  8037  curry2  8040  mapfoss  8779  bren  8882  en1  8949  fopwdom  9002  domss2  9053  mapen  9058  ssenen  9068  ssfiALT  9088  phplem2  9119  php3  9123  fodomfib  9219  fodomfibOLD  9221  f1opwfi  9246  ordiso2  9407  ordtypelem10  9419  oismo  9432  brwdom  9459  brwdom2  9465  wdomtr  9467  unxpwdom2  9480  wemapwe  9593  infxpenc2lem1  9913  fseqen  9921  fodomfi2  9954  infpwfien  9956  infmap2  10111  ackbij2  10136  infpssr  10202  fodomb  10420  fpwwe2lem5  10529  fpwwe2lem8  10532  tskuni  10677  gruen  10706  supcvg  15763  ruclem13  16151  unbenlem  16820  imasval  17415  imasaddfnlem  17432  imasvscafn  17441  imasless  17444  xpsfrn  17472  fulloppc  17831  imasmnd2  18648  resgrpplusfrn  18829  imasgrp2  18934  oppglsm  19521  efgrelexlemb  19629  gsumzres  19788  gsumzcl2  19789  gsumzf1o  19791  gsumzaddlem  19800  gsumconst  19813  gsumzmhm  19816  gsumzoppg  19823  dprdf1o  19913  imasrng  20062  imasring  20215  gsumfsum  21341  zncyg  21455  znf1o  21458  znleval  21461  znunit  21470  cygznlem2a  21474  indlcim  21747  cmpfi  23293  cnconn  23307  1stcfb  23330  qtopval2  23581  basqtop  23596  tgqtop  23597  imastopn  23605  hmeontr  23654  hmeoqtop  23660  nrmhmph  23679  cmphaushmeo  23685  elfm3  23835  qustgpopn  24005  tsmsf1o  24030  imasf1oxmet  24261  imasf1omet  24262  imasf1oxms  24375  cnheiborlem  24851  ovolctb  25389  dyadmbl  25499  dvcnvrelem2  25921  dvcnvre  25922  efifo  26454  circgrp  26459  circsubm  26460  logrn  26465  dvrelog  26544  efopnlem2  26564  fsumdvdsmul  27103  fsumdvdsmulOLD  27105  bdayimaon  27603  noetasuplem4  27646  noetainflem4  27650  bdayrn  27685  noeta2  27695  negsunif  27966  negsbdaylem  27967  zssno  28274  f1otrg  28816  axcontlem10  28918  isgrpo  30441  isgrpoi  30442  pjrn  31651  padct  32662  cycpmconjvlem  33083  cycpmconjslem2  33097  imaslmod  33290  qusdimsum  33595  sigapildsys  34129  carsgclctunlem3  34288  ballotlemro  34491  erdsze2lem1  35176  cnpconn  35203  poimirlem15  37615  mblfinlem2  37638  volsupnfl  37645  ismtyres  37788  rngopidOLD  37833  opidon2OLD  37834  rngmgmbs4  37911  isgrpda  37935  mapdrn  41628  ricdrng1  42501  dnnumch2  43018  lnmlmic  43061  pwslnmlem1  43065  pwslnmlem2  43066  ntrneifv2  44053  ssnnf1octb  45172  stoweidlem27  46008  fourierdlem51  46138  fourierdlem102  46189  fourierdlem114  46201  sge0fodjrnlem  46397  nnfoctbdjlem  46436  nnfoctbdj  46437  3f1oss1  47059  fonex  48851  tposres3  48865