Theorem forn 6775

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

Syntax hints:   → wi 4   = wceq 1540  ran crn 5639   Fn wfn 6506  –onto→wfo 6509

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 6517

This theorem is referenced by:  dffo2  6776  foima  6777  fodmrnu  6780  focnvimacdmdm  6784  focofo  6785  foco  6786  f1imacnv  6816  foimacnv  6817  foun  6818  resdif  6821  fococnv2  6826  foelcdmi  6922  f1ounsn  7247  cbvfo  7264  f1ocoima  7278  isoini  7313  isofrlem  7315  isoselem  7316  canth  7341  f1opw2  7644  focdmex  7934  wemoiso2  7953  curry1  8083  curry2  8086  mapfoss  8825  bren  8928  en1  8995  fopwdom  9049  domss2  9100  mapen  9105  ssenen  9115  ssfiALT  9138  phplem2  9169  php3  9173  fodomfib  9280  fodomfibOLD  9282  f1opwfi  9307  ordiso2  9468  ordtypelem10  9480  oismo  9493  brwdom  9520  brwdom2  9526  wdomtr  9528  unxpwdom2  9541  wemapwe  9650  infxpenc2lem1  9972  fseqen  9980  fodomfi2  10013  infpwfien  10015  infmap2  10170  ackbij2  10195  infpssr  10261  fodomb  10479  fpwwe2lem5  10588  fpwwe2lem8  10591  tskuni  10736  gruen  10765  supcvg  15822  ruclem13  16210  unbenlem  16879  imasval  17474  imasaddfnlem  17491  imasvscafn  17500  imasless  17503  xpsfrn  17531  fulloppc  17886  imasmnd2  18701  resgrpplusfrn  18882  imasgrp2  18987  oppglsm  19572  efgrelexlemb  19680  gsumzres  19839  gsumzcl2  19840  gsumzf1o  19842  gsumzaddlem  19851  gsumconst  19864  gsumzmhm  19867  gsumzoppg  19874  dprdf1o  19964  imasrng  20086  imasring  20239  gsumfsum  21351  zncyg  21458  znf1o  21461  znleval  21464  znunit  21473  cygznlem2a  21477  indlcim  21749  cmpfi  23295  cnconn  23309  1stcfb  23332  qtopval2  23583  basqtop  23598  tgqtop  23599  imastopn  23607  hmeontr  23656  hmeoqtop  23662  nrmhmph  23681  cmphaushmeo  23687  elfm3  23837  qustgpopn  24007  tsmsf1o  24032  imasf1oxmet  24263  imasf1omet  24264  imasf1oxms  24377  cnheiborlem  24853  ovolctb  25391  dyadmbl  25501  dvcnvrelem2  25923  dvcnvre  25924  efifo  26456  circgrp  26461  circsubm  26462  logrn  26467  dvrelog  26546  efopnlem2  26566  fsumdvdsmul  27105  fsumdvdsmulOLD  27107  bdayimaon  27605  noetasuplem4  27648  noetainflem4  27652  bdayrn  27687  noeta2  27696  negsunif  27961  negsbdaylem  27962  zssno  28269  f1otrg  28798  axcontlem10  28900  isgrpo  30426  isgrpoi  30427  pjrn  31636  padct  32643  cycpmconjvlem  33098  cycpmconjslem2  33112  imaslmod  33324  qusdimsum  33624  sigapildsys  34152  carsgclctunlem3  34311  ballotlemro  34514  erdsze2lem1  35190  cnpconn  35217  poimirlem15  37629  mblfinlem2  37652  volsupnfl  37659  ismtyres  37802  rngopidOLD  37847  opidon2OLD  37848  rngmgmbs4  37925  isgrpda  37949  mapdrn  41643  ricdrng1  42516  dnnumch2  43034  lnmlmic  43077  pwslnmlem1  43081  pwslnmlem2  43082  ntrneifv2  44069  ssnnf1octb  45188  stoweidlem27  46025  fourierdlem51  46155  fourierdlem102  46206  fourierdlem114  46218  sge0fodjrnlem  46414  nnfoctbdjlem  46453  nnfoctbdj  46454  3f1oss1  47076  fonex  48855  tposres3  48869