Theorem forn 6795

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

Syntax hints:   → wi 4   = wceq 1570  ran crn 5662   Fn wfn 6531  –onto→wfo 6534

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 210  df-an 401  df-fo 6542

This theorem is referenced by:  dffo2  6796  foima  6797  fodmrnu  6800  focnvimacdmdm  6804  focofo  6805  foco  6806  f1imacnv  6837  foimacnv  6838  foun  6839  resdif  6842  fococnv2  6847  foelcdmi  6942  f1ounsn  7270  cbvfo  7287  f1ocoima  7301  isoini  7336  isofrlem  7338  isoselem  7339  canth  7364  f1opw2  7665  focdmex  7949  wemoiso2  7967  curry1  8095  curry2  8098  mapfoss  8845  bren  8949  en1  9017  fopwdom  9069  domss2  9120  mapen  9125  ssenen  9135  ssfiALT  9154  phplem2  9185  php3  9189  fodomfib  9284  f1opwfi  9309  ordiso2  9473  ordtypelem10  9485  oismo  9498  brwdom  9525  brwdom2  9531  wdomtr  9533  unxpwdom2  9546  wemapwe  9662  infxpenc2lem1  9999  fseqen  10007  fodomfi2  10040  infpwfien  10042  infmap2  10196  ackbij2  10221  infpssr  10287  fodomb  10505  fpwwe2lem5  10615  fpwwe2lem8  10618  tskuni  10763  gruen  10792  supcvg  15906  ruclem13  16293  unbenlem  16963  imasval  17560  imasaddfnlem  17577  imasvscafn  17586  imasless  17589  xpsfrn  17617  fulloppc  17976  imasmnd2  18827  resgrpplusfrn  19012  imasgrp2  19116  oppglsm  19707  efgrelexlemb  19815  gsumzres  19974  gsumzcl2  19975  gsumzf1o  19977  gsumzaddlem  19986  gsumconst  19999  gsumzmhm  20002  gsumzoppg  20009  dprdf1o  20099  imasrng  20250  imasring  20408  gsumfsum  21584  zncyg  21698  znf1o  21701  znleval  21704  znunit  21713  cygznlem2a  21717  indlcim  21990  cmpfi  23565  cnconn  23579  1stcfb  23602  qtopval2  23853  basqtop  23868  tgqtop  23869  imastopn  23877  hmeontr  23926  hmeoqtop  23932  nrmhmph  23951  cmphaushmeo  23957  elfm3  24107  qustgpopn  24277  tsmsf1o  24302  imasf1oxmet  24532  imasf1omet  24533  imasf1oxms  24646  cnheiborlem  25113  ovolctb  25649  dyadmbl  25759  dvcnvrelem2  26177  dvcnvre  26178  efifo  26712  circgrp  26717  circsubm  26718  logrn  26723  dvrelog  26802  efopnlem2  26822  fsumdvdsmul  27359  bdayimaon  27857  noetasuplem4  27900  noetainflem4  27904  bdayrn  27944  noeta2  27954  negsunif  28248  negbdaylem  28249  zssno  28574  f1otrg  29220  axcontlem10  29323  isgrpo  30849  isgrpoi  30850  pjrn  32059  padct  33063  cycpmconjvlem  33461  cycpmconjslem2  33475  imaslmod  33673  esplysply  33961  qusdimsum  34018  sigapildsys  34552  carsgclctunlem3  34710  ballotlemro  34913  onvfowev  35600  erdsze2lem1  35695  cnpconn  35722  poimirlem15  38286  mblfinlem2  38309  volsupnfl  38316  ismtyres  38459  rngopidOLD  38504  opidon2OLD  38505  rngmgmbs4  38582  isgrpda  38606  mapdrn  42423  ricdrng1  43296  dnnumch2  43772  lnmlmic  43815  pwslnmlem1  43819  pwslnmlem2  43820  ntrneifv2  44806  ssnnf1octb  45912  stoweidlem27  46741  fourierdlem51  46871  fourierdlem102  46922  fourierdlem114  46934  sge0fodjrnlem  47130  nnfoctbdjlem  47169  nnfoctbdj  47170  3f1oss1  47812  fonex  49645  tposres3  49659