Theorem forn 6809

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

Syntax hints:   → wi 4   = wceq 1542  ran crn 5678   Fn wfn 6539  –onto→wfo 6542

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 398  df-fo 6550

This theorem is referenced by:  dffo2  6810  foima  6811  fodmrnu  6814  focnvimacdmdm  6818  focofo  6819  foco  6820  f1imacnv  6850  foimacnv  6851  foun  6852  resdif  6855  fococnv2  6860  foelcdmi  6954  cbvfo  7287  isoini  7335  isofrlem  7337  isoselem  7338  canth  7362  f1opw2  7661  focdmex  7942  wemoiso2  7961  curry1  8090  curry2  8093  mapfoss  8846  bren  8949  brenOLD  8950  en1  9021  en1OLD  9022  fopwdom  9080  domss2  9136  mapen  9141  ssenen  9151  ssfiALT  9174  phplem2  9208  php3  9212  phplem4OLD  9220  php3OLD  9224  fodomfib  9326  f1opwfi  9356  ordiso2  9510  ordtypelem10  9522  oismo  9535  brwdom  9562  brwdom2  9568  wdomtr  9570  unxpwdom2  9583  wemapwe  9692  infxpenc2lem1  10014  fseqen  10022  fodomfi2  10055  infpwfien  10057  infmap2  10213  ackbij2  10238  infpssr  10303  fodomb  10521  fpwwe2lem5  10630  fpwwe2lem8  10633  tskuni  10778  gruen  10807  hashfacenOLD  14414  supcvg  15802  ruclem13  16185  unbenlem  16841  imasval  17457  imasaddfnlem  17474  imasvscafn  17483  imasless  17486  xpsfrn  17514  fulloppc  17873  imasmnd2  18662  resgrpplusfrn  18836  imasgrp2  18938  oppglsm  19510  efgrelexlemb  19618  gsumzres  19777  gsumzcl2  19778  gsumzf1o  19780  gsumzaddlem  19789  gsumconst  19802  gsumzmhm  19805  gsumzoppg  19812  dprdf1o  19902  imasring  20143  gsumfsum  21012  zncyg  21104  znf1o  21107  znleval  21110  znunit  21119  cygznlem2a  21123  indlcim  21395  cmpfi  22912  cnconn  22926  1stcfb  22949  qtopval2  23200  basqtop  23215  tgqtop  23216  imastopn  23224  hmeontr  23273  hmeoqtop  23279  nrmhmph  23298  cmphaushmeo  23304  elfm3  23454  qustgpopn  23624  tsmsf1o  23649  imasf1oxmet  23881  imasf1omet  23882  imasf1oxms  23998  cnheiborlem  24470  ovolctb  25007  dyadmbl  25117  dvcnvrelem2  25535  dvcnvre  25536  efifo  26056  circgrp  26061  circsubm  26062  logrn  26067  dvrelog  26145  efopnlem2  26165  fsumdvdsmul  26699  bdayimaon  27196  noetasuplem4  27239  noetainflem4  27243  bdayrn  27277  noeta2  27286  negsunif  27529  negsbdaylem  27530  f1otrg  28122  axcontlem10  28231  isgrpo  29750  isgrpoi  29751  pjrn  30960  padct  31944  cycpmconjvlem  32300  cycpmconjslem2  32314  imaslmod  32468  qusdimsum  32713  sigapildsys  33160  carsgclctunlem3  33319  ballotlemro  33521  erdsze2lem1  34194  cnpconn  34221  poimirlem15  36503  mblfinlem2  36526  volsupnfl  36533  ismtyres  36676  rngopidOLD  36721  opidon2OLD  36722  rngmgmbs4  36799  isgrpda  36823  mapdrn  40520  ricdrng1  41102  dnnumch2  41787  lnmlmic  41830  pwslnmlem1  41834  pwslnmlem2  41835  ntrneifv2  42831  ssnnf1octb  43893  stoweidlem27  44743  fourierdlem51  44873  fourierdlem102  44924  fourierdlem114  44936  sge0fodjrnlem  45132  nnfoctbdjlem  45171  nnfoctbdj  45172  imasrng  46678