Theorem forn 5798

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

Syntax hints:   -> wi 4   = wceq 1379   ran crn 5000   Fn wfn 5583   -onto->wfo 5586

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 5594

This theorem is referenced by:  dffo2  5799  foima  5800  fodmrnu  5803  f1imacnv  5832  foimacnv  5833  foun  5834  resdif  5836  fococnv2  5841  cbvfo  6180  isoini  6222  isofrlem  6224  isoselem  6225  canth  6242  f1opw2  6512  fornex  6753  wemoiso2  6770  curry1  6875  curry2  6878  bren  7525  en1  7582  fopwdom  7625  domss2  7676  mapen  7681  ssenen  7691  phplem4  7699  php3  7703  ssfi  7740  fodomfib  7800  f1opwfi  7824  ordiso2  7940  ordtypelem10  7952  oismo  7965  brwdom  7993  brwdom2  7999  wdomtr  8001  unxpwdom2  8014  wemapwe  8139  wemapweOLD  8140  infxpenc2lem1  8396  fseqen  8408  fodomfi2  8441  infpwfien  8443  infmap2  8598  ackbij2  8623  infpssr  8688  fodomb  8904  fpwwe2lem6  9013  fpwwe2lem9  9016  tskuni  9161  gruen  9190  hashfacen  12469  supcvg  13630  ruclem13  13836  unbenlem  14285  imasval  14766  imasaddfnlem  14783  imasvscafn  14792  imasless  14795  xpsfrn  14824  fulloppc  15149  imasmnd2  15776  imasgrp2  15995  oppglsm  16468  efgrelexlemb  16574  gsumzres  16717  gsumzcl2  16718  gsumzf1o  16720  gsumzresOLD  16721  gsumzclOLD  16722  gsumzf1oOLD  16723  gsumzaddlem  16737  gsumzaddlemOLD  16739  gsumconst  16757  gsumzmhm  16760  gsumzmhmOLD  16761  gsumzoppg  16770  gsumzoppgOLD  16771  dprdf1o  16881  imasrng  17069  gsumfsum  18280  zncyg  18382  znf1o  18385  znleval  18388  znunit  18397  cygznlem2a  18401  indlcim  18670  cmpfi  19702  cnconn  19717  1stcfb  19740  qtopval2  19960  basqtop  19975  tgqtop  19976  imastopn  19984  hmeontr  20033  hmeoqtop  20039  nrmhmph  20058  cmphaushmeo  20064  elfm3  20214  divstgpopn  20381  tsmsf1o  20410  imasf1oxmet  20641  imasf1omet  20642  imasf1oxms  20755  cnheiborlem  21217  ovolctb  21664  dyadmbl  21772  dvcnvrelem2  22182  dvcnvre  22183  efifo  22695  logrn  22702  dvrelog  22774  efopnlem2  22794  fsumdvdsmul  23227  f1otrg  23878  axcontlem10  23980  eupares  24679  eupath2lem3  24683  isgrpo  24902  isgrpoi  24904  isgrp2d  24941  isgrpda  25003  rngopid  25029  opidon2  25030  circgrp  25080  rngmgmbs4  25123  pjrn  26329  ballotlemro  28129  erdsze2lem1  28315  cnpcon  28343  bdayrn  29042  mblfinlem2  29657  volsupnfl  29664  ismtyres  29935  dnnumch2  30623  lnmlmic  30666  pwslnmlem1  30670  pwslnmlem2  30671  stoweidlem27  31355  fourierdlem51  31486  fourierdlem102  31537  fourierdlem114  31549  mapdrn  36464