Theorem forn 6823

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

Syntax hints:   → wi 4   = wceq 1540  ran crn 5686   Fn wfn 6556  –onto→wfo 6559

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 6567

This theorem is referenced by:  dffo2  6824  foima  6825  fodmrnu  6828  focnvimacdmdm  6832  focofo  6833  foco  6834  f1imacnv  6864  foimacnv  6865  foun  6866  resdif  6869  fococnv2  6874  foelcdmi  6970  f1ounsn  7292  cbvfo  7309  f1ocoima  7323  isoini  7358  isofrlem  7360  isoselem  7361  canth  7385  f1opw2  7688  focdmex  7980  wemoiso2  7999  curry1  8129  curry2  8132  mapfoss  8892  bren  8995  en1  9064  fopwdom  9120  domss2  9176  mapen  9181  ssenen  9191  ssfiALT  9214  phplem2  9245  php3  9249  phplem4OLD  9257  php3OLD  9261  fodomfib  9369  fodomfibOLD  9371  f1opwfi  9396  ordiso2  9555  ordtypelem10  9567  oismo  9580  brwdom  9607  brwdom2  9613  wdomtr  9615  unxpwdom2  9628  wemapwe  9737  infxpenc2lem1  10059  fseqen  10067  fodomfi2  10100  infpwfien  10102  infmap2  10257  ackbij2  10282  infpssr  10348  fodomb  10566  fpwwe2lem5  10675  fpwwe2lem8  10678  tskuni  10823  gruen  10852  supcvg  15892  ruclem13  16278  unbenlem  16946  imasval  17556  imasaddfnlem  17573  imasvscafn  17582  imasless  17585  xpsfrn  17613  fulloppc  17969  imasmnd2  18787  resgrpplusfrn  18968  imasgrp2  19073  oppglsm  19660  efgrelexlemb  19768  gsumzres  19927  gsumzcl2  19928  gsumzf1o  19930  gsumzaddlem  19939  gsumconst  19952  gsumzmhm  19955  gsumzoppg  19962  dprdf1o  20052  imasrng  20174  imasring  20327  gsumfsum  21452  zncyg  21567  znf1o  21570  znleval  21573  znunit  21582  cygznlem2a  21586  indlcim  21860  cmpfi  23416  cnconn  23430  1stcfb  23453  qtopval2  23704  basqtop  23719  tgqtop  23720  imastopn  23728  hmeontr  23777  hmeoqtop  23783  nrmhmph  23802  cmphaushmeo  23808  elfm3  23958  qustgpopn  24128  tsmsf1o  24153  imasf1oxmet  24385  imasf1omet  24386  imasf1oxms  24502  cnheiborlem  24986  ovolctb  25525  dyadmbl  25635  dvcnvrelem2  26057  dvcnvre  26058  efifo  26589  circgrp  26594  circsubm  26595  logrn  26600  dvrelog  26679  efopnlem2  26699  fsumdvdsmul  27238  fsumdvdsmulOLD  27240  bdayimaon  27738  noetasuplem4  27781  noetainflem4  27785  bdayrn  27820  noeta2  27829  negsunif  28087  negsbdaylem  28088  zssno  28367  f1otrg  28879  axcontlem10  28988  isgrpo  30516  isgrpoi  30517  pjrn  31726  padct  32731  cycpmconjvlem  33161  cycpmconjslem2  33175  imaslmod  33381  qusdimsum  33679  sigapildsys  34163  carsgclctunlem3  34322  ballotlemro  34525  erdsze2lem1  35208  cnpconn  35235  poimirlem15  37642  mblfinlem2  37665  volsupnfl  37672  ismtyres  37815  rngopidOLD  37860  opidon2OLD  37861  rngmgmbs4  37938  isgrpda  37962  mapdrn  41651  ricdrng1  42538  dnnumch2  43057  lnmlmic  43100  pwslnmlem1  43104  pwslnmlem2  43105  ntrneifv2  44093  ssnnf1octb  45199  stoweidlem27  46042  fourierdlem51  46172  fourierdlem102  46223  fourierdlem114  46235  sge0fodjrnlem  46431  nnfoctbdjlem  46470  nnfoctbdj  46471  3f1oss1  47087  uspgrimprop  47873  tposres3  48781