Theorem forn 6747

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

Syntax hints:   → wi 4   = wceq 1541  ran crn 5623   Fn wfn 6485  –onto→wfo 6488

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 6496

This theorem is referenced by:  dffo2  6748  foima  6749  fodmrnu  6752  focnvimacdmdm  6756  focofo  6757  foco  6758  f1imacnv  6788  foimacnv  6789  foun  6790  resdif  6793  fococnv2  6798  foelcdmi  6893  f1ounsn  7216  cbvfo  7233  f1ocoima  7247  isoini  7282  isofrlem  7284  isoselem  7285  canth  7310  f1opw2  7611  focdmex  7898  wemoiso2  7916  curry1  8044  curry2  8047  mapfoss  8787  bren  8891  en1  8959  fopwdom  9011  domss2  9062  mapen  9067  ssenen  9077  ssfiALT  9096  phplem2  9127  php3  9131  fodomfib  9227  fodomfibOLD  9229  f1opwfi  9254  ordiso2  9418  ordtypelem10  9430  oismo  9443  brwdom  9470  brwdom2  9476  wdomtr  9478  unxpwdom2  9491  wemapwe  9604  infxpenc2lem1  9927  fseqen  9935  fodomfi2  9968  infpwfien  9970  infmap2  10125  ackbij2  10150  infpssr  10216  fodomb  10434  fpwwe2lem5  10544  fpwwe2lem8  10547  tskuni  10692  gruen  10721  supcvg  15777  ruclem13  16165  unbenlem  16834  imasval  17430  imasaddfnlem  17447  imasvscafn  17456  imasless  17459  xpsfrn  17487  fulloppc  17846  imasmnd2  18697  resgrpplusfrn  18878  imasgrp2  18983  oppglsm  19569  efgrelexlemb  19677  gsumzres  19836  gsumzcl2  19837  gsumzf1o  19839  gsumzaddlem  19848  gsumconst  19861  gsumzmhm  19864  gsumzoppg  19871  dprdf1o  19961  imasrng  20110  imasring  20264  gsumfsum  21387  zncyg  21501  znf1o  21504  znleval  21507  znunit  21516  cygznlem2a  21520  indlcim  21793  cmpfi  23350  cnconn  23364  1stcfb  23387  qtopval2  23638  basqtop  23653  tgqtop  23654  imastopn  23662  hmeontr  23711  hmeoqtop  23717  nrmhmph  23736  cmphaushmeo  23742  elfm3  23892  qustgpopn  24062  tsmsf1o  24087  imasf1oxmet  24317  imasf1omet  24318  imasf1oxms  24431  cnheiborlem  24907  ovolctb  25445  dyadmbl  25555  dvcnvrelem2  25977  dvcnvre  25978  efifo  26510  circgrp  26515  circsubm  26516  logrn  26521  dvrelog  26600  efopnlem2  26620  fsumdvdsmul  27159  fsumdvdsmulOLD  27161  bdayimaon  27659  noetasuplem4  27702  noetainflem4  27706  bdayrn  27741  noeta2  27751  negsunif  28024  negsbdaylem  28025  zssno  28339  f1otrg  28892  axcontlem10  28995  isgrpo  30521  isgrpoi  30522  pjrn  31731  padct  32746  cycpmconjvlem  33172  cycpmconjslem2  33186  imaslmod  33383  esplysply  33678  qusdimsum  33734  sigapildsys  34268  carsgclctunlem3  34426  ballotlemro  34629  erdsze2lem1  35346  cnpconn  35373  poimirlem15  37775  mblfinlem2  37798  volsupnfl  37805  ismtyres  37948  rngopidOLD  37993  opidon2OLD  37994  rngmgmbs4  38071  isgrpda  38095  mapdrn  41848  ricdrng1  42725  dnnumch2  43229  lnmlmic  43272  pwslnmlem1  43276  pwslnmlem2  43277  ntrneifv2  44263  ssnnf1octb  45380  stoweidlem27  46213  fourierdlem51  46343  fourierdlem102  46394  fourierdlem114  46406  sge0fodjrnlem  46602  nnfoctbdjlem  46641  nnfoctbdj  46642  3f1oss1  47263  fonex  49054  tposres3  49068