Theorem forn 6757

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

Syntax hints:   → wi 4   = wceq 1542  ran crn 5633   Fn wfn 6495  –onto→wfo 6498

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 6506

This theorem is referenced by:  dffo2  6758  foima  6759  fodmrnu  6762  focnvimacdmdm  6766  focofo  6767  foco  6768  f1imacnv  6798  foimacnv  6799  foun  6800  resdif  6803  fococnv2  6808  foelcdmi  6903  f1ounsn  7228  cbvfo  7245  f1ocoima  7259  isoini  7294  isofrlem  7296  isoselem  7297  canth  7322  f1opw2  7623  focdmex  7910  wemoiso2  7928  curry1  8056  curry2  8059  mapfoss  8801  bren  8905  en1  8973  fopwdom  9025  domss2  9076  mapen  9081  ssenen  9091  ssfiALT  9110  phplem2  9141  php3  9145  fodomfib  9241  fodomfibOLD  9243  f1opwfi  9268  ordiso2  9432  ordtypelem10  9444  oismo  9457  brwdom  9484  brwdom2  9490  wdomtr  9492  unxpwdom2  9505  wemapwe  9618  infxpenc2lem1  9941  fseqen  9949  fodomfi2  9982  infpwfien  9984  infmap2  10139  ackbij2  10164  infpssr  10230  fodomb  10448  fpwwe2lem5  10558  fpwwe2lem8  10561  tskuni  10706  gruen  10735  supcvg  15791  ruclem13  16179  unbenlem  16848  imasval  17444  imasaddfnlem  17461  imasvscafn  17470  imasless  17473  xpsfrn  17501  fulloppc  17860  imasmnd2  18711  resgrpplusfrn  18892  imasgrp2  18997  oppglsm  19583  efgrelexlemb  19691  gsumzres  19850  gsumzcl2  19851  gsumzf1o  19853  gsumzaddlem  19862  gsumconst  19875  gsumzmhm  19878  gsumzoppg  19885  dprdf1o  19975  imasrng  20124  imasring  20278  gsumfsum  21401  zncyg  21515  znf1o  21518  znleval  21521  znunit  21530  cygznlem2a  21534  indlcim  21807  cmpfi  23364  cnconn  23378  1stcfb  23401  qtopval2  23652  basqtop  23667  tgqtop  23668  imastopn  23676  hmeontr  23725  hmeoqtop  23731  nrmhmph  23750  cmphaushmeo  23756  elfm3  23906  qustgpopn  24076  tsmsf1o  24101  imasf1oxmet  24331  imasf1omet  24332  imasf1oxms  24445  cnheiborlem  24921  ovolctb  25459  dyadmbl  25569  dvcnvrelem2  25991  dvcnvre  25992  efifo  26524  circgrp  26529  circsubm  26530  logrn  26535  dvrelog  26614  efopnlem2  26634  fsumdvdsmul  27173  fsumdvdsmulOLD  27175  bdayimaon  27673  noetasuplem4  27716  noetainflem4  27720  bdayrn  27759  noeta2  27769  negsunif  28063  negbdaylem  28064  zssno  28389  f1otrg  28955  axcontlem10  29058  isgrpo  30585  isgrpoi  30586  pjrn  31795  padct  32808  cycpmconjvlem  33235  cycpmconjslem2  33249  imaslmod  33446  esplysply  33748  qusdimsum  33806  sigapildsys  34340  carsgclctunlem3  34498  ballotlemro  34701  erdsze2lem1  35419  cnpconn  35446  poimirlem15  37886  mblfinlem2  37909  volsupnfl  37916  ismtyres  38059  rngopidOLD  38104  opidon2OLD  38105  rngmgmbs4  38182  isgrpda  38206  mapdrn  42025  ricdrng1  42898  dnnumch2  43402  lnmlmic  43445  pwslnmlem1  43449  pwslnmlem2  43450  ntrneifv2  44436  ssnnf1octb  45553  stoweidlem27  46385  fourierdlem51  46515  fourierdlem102  46566  fourierdlem114  46578  sge0fodjrnlem  46774  nnfoctbdjlem  46813  nnfoctbdj  46814  3f1oss1  47435  fonex  49226  tposres3  49240