Theorem forn 5611

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 5412	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
2	1	simprbi 461	1 |- ( F : A -onto-> B -> ran F = B )

Syntax hints:   -> wi 4   = wceq 1362   ran crn 4828   Fn wfn 5401   -onto->wfo 5404

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 185  df-an 371  df-fo 5412

This theorem is referenced by:  dffo2  5612  foima  5613  fodmrnu  5616  f1imacnv  5645  foimacnv  5646  foun  5647  resdif  5649  fococnv2  5654  cbvfo  5980  isoini  6016  isofrlem  6018  isoselem  6019  canth  6036  f1opw2  6302  fornex  6535  wemoiso2  6552  curry1  6653  curry2  6656  bren  7307  en1  7364  fopwdom  7407  domss2  7458  mapen  7463  ssenen  7473  phplem4  7481  php3  7485  ssfi  7521  fodomfib  7579  f1opwfi  7603  ordiso2  7717  ordtypelem10  7729  oismo  7742  brwdom  7770  brwdom2  7776  wdomtr  7778  unxpwdom2  7791  wemapwe  7916  wemapweOLD  7917  infxpenc2lem1  8173  fseqen  8185  fodomfi2  8218  infpwfien  8220  infmap2  8375  ackbij2  8400  infpssr  8465  fodomb  8681  fpwwe2lem6  8790  fpwwe2lem9  8793  tskuni  8938  gruen  8967  hashfacen  12191  supcvg  13301  ruclem13  13507  unbenlem  13952  imasval  14432  imasaddfnlem  14449  imasvscafn  14458  imasless  14461  xpsfrn  14490  fulloppc  14815  imasmnd2  15441  imasgrp2  15650  oppglsm  16121  efgrelexlemb  16227  gsumzres  16368  gsumzcl2  16369  gsumzf1o  16371  gsumzresOLD  16372  gsumzclOLD  16373  gsumzf1oOLD  16374  gsumzaddlem  16388  gsumzaddlemOLD  16390  gsumconst  16406  gsumzmhm  16407  gsumzmhmOLD  16408  gsumzoppg  16416  gsumzoppgOLD  16417  dprdf1o  16503  imasrng  16646  gsumfsum  17723  zncyg  17823  znf1o  17826  znleval  17829  znunit  17838  cygznlem2a  17842  indlcim  18111  cmpfi  18853  cnconn  18868  1stcfb  18891  qtopval2  19111  basqtop  19126  tgqtop  19127  imastopn  19135  hmeontr  19184  hmeoqtop  19190  nrmhmph  19209  cmphaushmeo  19215  elfm3  19365  divstgpopn  19532  tsmsf1o  19561  imasf1oxmet  19792  imasf1omet  19793  imasf1oxms  19906  cnheiborlem  20368  ovolctb  20815  dyadmbl  20922  dvcnvrelem2  21332  dvcnvre  21333  efifo  21888  logrn  21895  dvrelog  21967  efopnlem2  21987  fsumdvdsmul  22420  f1otrg  22940  axcontlem10  23042  eupares  23419  eupath2lem3  23423  isgrpo  23506  isgrpoi  23508  isgrp2d  23545  isgrpda  23607  rngopid  23633  opidon2  23634  circgrp  23684  rngmgmbs4  23727  pjrn  24933  ballotlemro  26753  erdsze2lem1  26939  cnpcon  26967  bdayrn  27665  mblfinlem2  28273  volsupnfl  28280  ismtyres  28551  dnnumch2  29243  lnmlmic  29286  pwslnmlem1  29290  pwslnmlem2  29291  stoweidlem27  29668  mapdrn  34867