Theorem forn 6675

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

Syntax hints:   → wi 4   = wceq 1539  ran crn 5581   Fn wfn 6413  –onto→wfo 6416

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 206  df-an 396  df-fo 6424

This theorem is referenced by:  dffo2  6676  foima  6677  fodmrnu  6680  focnvimacdmdm  6684  focofo  6685  foco  6686  f1imacnv  6716  foimacnv  6717  foun  6718  resdif  6720  fococnv2  6725  foelrni  6813  cbvfo  7141  isoini  7189  isofrlem  7191  isoselem  7192  canth  7209  f1opw2  7502  fornex  7772  wemoiso2  7790  curry1  7915  curry2  7918  mapfoss  8598  bren  8701  brenOLD  8702  en1  8765  en1OLD  8766  fopwdom  8820  domss2  8872  mapen  8877  ssenen  8887  phplem4  8895  php3  8899  ssfiALT  8919  fodomfib  9023  f1opwfi  9053  ordiso2  9204  ordtypelem10  9216  oismo  9229  brwdom  9256  brwdom2  9262  wdomtr  9264  unxpwdom2  9277  wemapwe  9385  infxpenc2lem1  9706  fseqen  9714  fodomfi2  9747  infpwfien  9749  infmap2  9905  ackbij2  9930  infpssr  9995  fodomb  10213  fpwwe2lem5  10322  fpwwe2lem8  10325  tskuni  10470  gruen  10499  focdmex  13993  hashfacenOLD  14095  supcvg  15496  ruclem13  15879  unbenlem  16537  imasval  17139  imasaddfnlem  17156  imasvscafn  17165  imasless  17168  xpsfrn  17196  fulloppc  17554  imasmnd2  18337  resgrpplusfrn  18508  imasgrp2  18605  oppglsm  19162  efgrelexlemb  19271  gsumzres  19425  gsumzcl2  19426  gsumzf1o  19428  gsumzaddlem  19437  gsumconst  19450  gsumzmhm  19453  gsumzoppg  19460  dprdf1o  19550  imasring  19773  gsumfsum  20577  zncyg  20668  znf1o  20671  znleval  20674  znunit  20683  cygznlem2a  20687  indlcim  20957  cmpfi  22467  cnconn  22481  1stcfb  22504  qtopval2  22755  basqtop  22770  tgqtop  22771  imastopn  22779  hmeontr  22828  hmeoqtop  22834  nrmhmph  22853  cmphaushmeo  22859  elfm3  23009  qustgpopn  23179  tsmsf1o  23204  imasf1oxmet  23436  imasf1omet  23437  imasf1oxms  23551  cnheiborlem  24023  ovolctb  24559  dyadmbl  24669  dvcnvrelem2  25087  dvcnvre  25088  efifo  25608  circgrp  25613  circsubm  25614  logrn  25619  dvrelog  25697  efopnlem2  25717  fsumdvdsmul  26249  f1otrg  27136  axcontlem10  27244  isgrpo  28760  isgrpoi  28761  pjrn  29970  padct  30956  cycpmconjvlem  31310  cycpmconjslem2  31324  imaslmod  31455  qusdimsum  31611  sigapildsys  32030  carsgclctunlem3  32187  ballotlemro  32389  erdsze2lem1  33065  cnpconn  33092  bdayimaon  33823  noetasuplem4  33866  noetainflem4  33870  bdayrn  33897  noeta2  33906  poimirlem15  35719  mblfinlem2  35742  volsupnfl  35749  ismtyres  35893  rngopidOLD  35938  opidon2OLD  35939  rngmgmbs4  36016  isgrpda  36040  mapdrn  39590  dnnumch2  40786  lnmlmic  40829  pwslnmlem1  40833  pwslnmlem2  40834  ntrneifv2  41579  ssnnf1octb  42622  stoweidlem27  43458  fourierdlem51  43588  fourierdlem102  43639  fourierdlem114  43651  sge0fodjrnlem  43844  nnfoctbdjlem  43883  nnfoctbdj  43884