Theorem forn 6749

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

Syntax hints:   → wi 4   = wceq 1542  ran crn 5625   Fn wfn 6487  –onto→wfo 6490

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 6498

This theorem is referenced by:  dffo2  6750  foima  6751  fodmrnu  6754  focnvimacdmdm  6758  focofo  6759  foco  6760  f1imacnv  6790  foimacnv  6791  foun  6792  resdif  6795  fococnv2  6800  foelcdmi  6895  f1ounsn  7220  cbvfo  7237  f1ocoima  7251  isoini  7286  isofrlem  7288  isoselem  7289  canth  7314  f1opw2  7615  focdmex  7902  wemoiso2  7920  curry1  8047  curry2  8050  mapfoss  8792  bren  8896  en1  8964  fopwdom  9016  domss2  9067  mapen  9072  ssenen  9082  ssfiALT  9101  phplem2  9132  php3  9136  fodomfib  9232  fodomfibOLD  9234  f1opwfi  9259  ordiso2  9423  ordtypelem10  9435  oismo  9448  brwdom  9475  brwdom2  9481  wdomtr  9483  unxpwdom2  9496  wemapwe  9609  infxpenc2lem1  9932  fseqen  9940  fodomfi2  9973  infpwfien  9975  infmap2  10130  ackbij2  10155  infpssr  10221  fodomb  10439  fpwwe2lem5  10549  fpwwe2lem8  10552  tskuni  10697  gruen  10726  supcvg  15812  ruclem13  16200  unbenlem  16870  imasval  17466  imasaddfnlem  17483  imasvscafn  17492  imasless  17495  xpsfrn  17523  fulloppc  17882  imasmnd2  18733  resgrpplusfrn  18917  imasgrp2  19022  oppglsm  19608  efgrelexlemb  19716  gsumzres  19875  gsumzcl2  19876  gsumzf1o  19878  gsumzaddlem  19887  gsumconst  19900  gsumzmhm  19903  gsumzoppg  19910  dprdf1o  20000  imasrng  20149  imasring  20301  gsumfsum  21424  zncyg  21538  znf1o  21541  znleval  21544  znunit  21553  cygznlem2a  21557  indlcim  21830  cmpfi  23383  cnconn  23397  1stcfb  23420  qtopval2  23671  basqtop  23686  tgqtop  23687  imastopn  23695  hmeontr  23744  hmeoqtop  23750  nrmhmph  23769  cmphaushmeo  23775  elfm3  23925  qustgpopn  24095  tsmsf1o  24120  imasf1oxmet  24350  imasf1omet  24351  imasf1oxms  24464  cnheiborlem  24931  ovolctb  25467  dyadmbl  25577  dvcnvrelem2  25995  dvcnvre  25996  efifo  26524  circgrp  26529  circsubm  26530  logrn  26535  dvrelog  26614  efopnlem2  26634  fsumdvdsmul  27172  bdayimaon  27671  noetasuplem4  27714  noetainflem4  27718  bdayrn  27757  noeta2  27767  negsunif  28061  negbdaylem  28062  zssno  28387  f1otrg  28953  axcontlem10  29056  isgrpo  30583  isgrpoi  30584  pjrn  31793  padct  32806  cycpmconjvlem  33217  cycpmconjslem2  33231  imaslmod  33428  esplysply  33730  qusdimsum  33788  sigapildsys  34322  carsgclctunlem3  34480  ballotlemro  34683  erdsze2lem1  35401  cnpconn  35428  poimirlem15  37970  mblfinlem2  37993  volsupnfl  38000  ismtyres  38143  rngopidOLD  38188  opidon2OLD  38189  rngmgmbs4  38266  isgrpda  38290  mapdrn  42109  ricdrng1  42987  dnnumch2  43491  lnmlmic  43534  pwslnmlem1  43538  pwslnmlem2  43539  ntrneifv2  44525  ssnnf1octb  45642  stoweidlem27  46473  fourierdlem51  46603  fourierdlem102  46654  fourierdlem114  46666  sge0fodjrnlem  46862  nnfoctbdjlem  46901  nnfoctbdj  46902  3f1oss1  47535  fonex  49354  tposres3  49368