Theorem forn 6829

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ran crn 5659   Fn wfn 6561  ⟶ontowfo 6564

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fo 6572

This theorem is used by:  dffo2  6830  foima  6831  fodmrnu  6834  focnvimacdmdm  6838  focofo  6839  foco  6840  f1imacnv  6871  foimacnv  6872  foun  6873  resdif  6876  fococnv2  6882  foelcdmi  6977  f1ounsn  7311  cbvfo  7328  f1ocoima  7342  isoini  7377  isofrlem  7379  isoselem  7380  canth  7405  f1opw2  7708  focdmex  8002  wemoiso2  8020  curry1  8152  curry2  8155  mapfoss  8912  bren  9021  en1  9089  fopwdom  9142  domss2  9193  mapen  9198  ssenen  9208  ssfiALT  9227  phplem2  9258  php3  9262  fodomfib  9358  f1opwfi  9383  ordiso2  9546  ordtypelem10  9558  oismo  9571  brwdom  9598  brwdom2  9604  wdomtr  9606  unxpwdom2  9619  wemapwe  9735  infxpenc2lem1  10137  fseqen  10145  fodomfi2  10178  infpwfien  10180  infmap2  10334  ackbij2  10359  infpssr  10425  fodomb  10644  fpwwe2lem5  10759  fpwwe2lem8  10762  tskuni  10907  gruen  10936  supcvg  16069  ruclem13  16454  unbenlem  17130  imasval  17733  imasaddfnlem  17750  imasvscafn  17759  imasless  17762  xpsfrn  17790  fulloppc  18149  mgmidprnd  18908  imasmgm2  18913  imasmnd2  19018  resgrpplusfrn  19211  imasgrp2  19315  oppglsm  19907  efgrelexlemb  20015  gsumzres  20174  gsumzcl2  20175  gsumzf1o  20177  gsumzaddlem  20186  gsumconst  20199  gsumzmhm  20202  gsumzoppg  20209  dprdf1o  20299  imasrng  20450  imasring  20611  gsumfsum  21794  zncyg  21909  znf1o  21912  znleval  21915  znunit  21924  cygznlem2a  21928  indlcim  22201  cmpfi  23781  cnconn  23795  1stcfb  23818  qtopval2  24070  basqtop  24085  tgqtop  24086  imastopn  24094  hmeontr  24143  hmeoqtop  24149  nrmhmph  24168  cmphaushmeo  24174  elfm3  24324  qustgpopn  24494  tsmsf1o  24519  imasf1oxmet  24749  imasf1omet  24750  imasf1oxms  24863  cnheiborlem  25330  ovolctb  25866  dyadmbl  25976  dvcnvrelem2  26393  dvcnvre  26394  efifo  26932  circgrp  26937  circsubm  26938  logrn  26943  dvrelog  27022  efopnlem2  27042  fsumdvdsmul  27579  bdayimaon  28107  noetasuplem4  28150  noetainflem4  28154  bdayrn  28194  negsunif  28498  negbdaylem  28499  zssno  28824  f1otrg  29505  axcontlem10  29608  isgrpo  31156  isgrpoi  31157  pjrn  32366  padct  33407  cycpmconjvlem  33801  cycpmconjslem2  33815  imaslmod  34018  esplysply  34314  qusdimsum  34371  sigapildsys  34906  carsgclctunlem3  35063  ballotlemro  35266  prconf1acwevd  36089  onvfowev  36091  erdsze2lem1  36176  cnpconn  36203  poimirlem15  38821  mblfinlem2  38844  volsupnfl  38851  ismtyres  39008  rngopidOLD  39053  opidon2OLD  39054  rngmgmbs4  39131  isgrpda  39155  mapdrn  42972  ricdrng1  43858  dnnumch2  44318  lnmlmic  44356  pwslnmlem1  44360  pwslnmlem2  44361  ntrneifv2  45341  ssnnf1octb  46482  stoweidlem27  47310  fourierdlem51  47440  fourierdlem102  47491  fourierdlem114  47503  sge0fodjrnlem  47699  nnfoctbdjlem  47738  nnfoctbdj  47739  3f1oss1  48418  fonex  50309  tposres3  50325