Theorem forn 5804

Description: The codomain of an onto function is its range. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
forn	|- ( F : A -onto-> B -> ran F = B )

Proof of Theorem forn

Step	Hyp	Ref	Expression
1		df-fo 5598	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
2	1	simprbi 465	1 |- ( F : A -onto-> B -> ran F = B )

Syntax hints:   -> wi 4   = wceq 1437   ran crn 4846   Fn wfn 5587   -onto->wfo 5590

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 188  df-an 372  df-fo 5598

This theorem is referenced by:  dffo2  5805  foima  5806  fodmrnu  5809  f1imacnv  5838  foimacnv  5839  foun  5840  resdif  5842  fococnv2  5847  foelrni  5920  cbvfo  6193  isoini  6235  isofrlem  6237  isoselem  6238  canth  6255  f1opw2  6527  fornex  6767  wemoiso2  6784  curry1  6890  curry2  6893  bren  7577  en1  7634  fopwdom  7677  domss2  7728  mapen  7733  ssenen  7743  phplem4  7751  php3  7755  ssfi  7789  fodomfib  7848  f1opwfi  7875  ordiso2  8021  ordtypelem10  8033  oismo  8046  brwdom  8073  brwdom2  8079  wdomtr  8081  unxpwdom2  8094  wemapwe  8192  infxpenc2lem1  8439  fseqen  8447  fodomfi2  8480  infpwfien  8482  infmap2  8637  ackbij2  8662  infpssr  8727  fodomb  8943  fpwwe2lem6  9049  fpwwe2lem9  9052  tskuni  9197  gruen  9226  hashfacen  12601  supcvg  13881  ruclem13  14261  unbenlem  14804  imasval  15361  imasaddfnlem  15378  imasvscafn  15387  imasless  15390  xpsfrn  15419  fulloppc  15771  imasmnd2  16517  imasgrp2  16745  oppglsm  17222  efgrelexlemb  17328  gsumzres  17471  gsumzcl2  17472  gsumzf1o  17474  gsumzaddlem  17482  gsumconst  17495  gsumzmhm  17498  gsumzoppg  17505  dprdf1o  17593  imasring  17775  gsumfsum  18962  zncyg  19043  znf1o  19046  znleval  19049  znunit  19058  cygznlem2a  19062  indlcim  19322  cmpfi  20347  cnconn  20361  1stcfb  20384  qtopval2  20635  basqtop  20650  tgqtop  20651  imastopn  20659  hmeontr  20708  hmeoqtop  20714  nrmhmph  20733  cmphaushmeo  20739  elfm3  20889  qustgpopn  21058  tsmsf1o  21083  imasf1oxmet  21314  imasf1omet  21315  imasf1oxms  21428  cnheiborlem  21871  ovolctb  22317  dyadmbl  22432  dvcnvrelem2  22844  dvcnvre  22845  efifo  23358  circgrp  23363  circsubm  23364  logrn  23370  dvrelog  23444  efopnlem2  23464  fsumdvdsmul  23984  f1otrg  24744  axcontlem10  24846  eupares  25545  eupath2lem3  25549  isgrpo  25766  isgrpoi  25768  isgrp2d  25805  isgrpda  25867  rngopidOLD  25893  opidon2OLD  25894  circgrpOLD  25944  rngmgmbs4  25987  pjrn  27192  padct  28147  sigapildsys  28820  carsgclctunlem3  28978  ballotlemro  29178  erdsze2lem1  29711  cnpcon  29738  bdayrn  30348  poimirlem15  31659  mblfinlem2  31682  volsupnfl  31689  ismtyres  31844  mapdrn  34926  dnnumch2  35613  lnmlmic  35656  pwslnmlem1  35660  pwslnmlem2  35661  stoweidlem27  37460  fourierdlem51  37593  fourierdlem102  37644  fourierdlem114  37656  sge0fodjrnlem  37796  nnfoctbdjlem  37806  nnfoctbdj  37807