Theorem forn 5796

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

Syntax hints:   -> wi 4   = wceq 1444   ran crn 4835   Fn wfn 5577   -onto->wfo 5580

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 189  df-an 373  df-fo 5588

This theorem is referenced by:  dffo2  5797  foima  5798  fodmrnu  5801  f1imacnv  5830  foimacnv  5831  foun  5832  resdif  5834  fococnv2  5839  foelrni  5913  cbvfo  6187  isoini  6229  isofrlem  6231  isoselem  6232  canth  6249  f1opw2  6522  fornex  6762  wemoiso2  6779  curry1  6888  curry2  6891  bren  7578  en1  7636  fopwdom  7680  domss2  7731  mapen  7736  ssenen  7746  phplem4  7754  php3  7758  ssfi  7792  fodomfib  7851  f1opwfi  7878  ordiso2  8030  ordtypelem10  8042  oismo  8055  brwdom  8082  brwdom2  8088  wdomtr  8090  unxpwdom2  8103  wemapwe  8202  infxpenc2lem1  8450  fseqen  8458  fodomfi2  8491  infpwfien  8493  infmap2  8648  ackbij2  8673  infpssr  8738  fodomb  8954  fpwwe2lem6  9060  fpwwe2lem9  9063  tskuni  9208  gruen  9237  hashfacen  12617  supcvg  13914  ruclem13  14294  unbenlem  14852  imasval  15411  imasvalOLD  15412  imasaddfnlem  15434  imasvscafn  15443  imasless  15446  xpsfrn  15475  fulloppc  15827  imasmnd2  16573  imasgrp2  16801  oppglsm  17294  efgrelexlemb  17400  gsumzres  17543  gsumzcl2  17544  gsumzf1o  17546  gsumzaddlem  17554  gsumconst  17567  gsumzmhm  17570  gsumzoppg  17577  dprdf1o  17665  imasring  17847  gsumfsum  19034  zncyg  19119  znf1o  19122  znleval  19125  znunit  19134  cygznlem2a  19138  indlcim  19398  cmpfi  20423  cnconn  20437  1stcfb  20460  qtopval2  20711  basqtop  20726  tgqtop  20727  imastopn  20735  hmeontr  20784  hmeoqtop  20790  nrmhmph  20809  cmphaushmeo  20815  elfm3  20965  qustgpopn  21134  tsmsf1o  21159  imasf1oxmet  21390  imasf1omet  21391  imasf1oxms  21504  cnheiborlem  21982  ovolctb  22443  dyadmbl  22558  dvcnvrelem2  22970  dvcnvre  22971  efifo  23496  circgrp  23501  circsubm  23502  logrn  23508  dvrelog  23582  efopnlem2  23602  fsumdvdsmul  24124  f1otrg  24901  axcontlem10  25003  eupares  25703  eupath2lem3  25707  isgrpo  25924  isgrpoi  25926  isgrp2d  25963  isgrpda  26025  rngopidOLD  26051  opidon2OLD  26052  circgrpOLD  26102  rngmgmbs4  26145  pjrn  27360  padct  28307  sigapildsys  28984  carsgclctunlem3  29152  ballotlemro  29355  ballotlemroOLD  29393  erdsze2lem1  29926  cnpcon  29953  bdayrn  30566  poimirlem15  31955  mblfinlem2  31978  volsupnfl  31985  ismtyres  32140  mapdrn  35217  dnnumch2  35903  lnmlmic  35946  pwslnmlem1  35950  pwslnmlem2  35951  ssnnf1octb  37470  stoweidlem27  37887  fourierdlem51  38021  fourierdlem102  38072  fourierdlem114  38084  sge0fodjrnlem  38258  nnfoctbdjlem  38293  nnfoctbdj  38294