Theorem forn 6593

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

Syntax hints:   → wi 4   = wceq 1537  ran crn 5556   Fn wfn 6350  –onto→wfo 6353

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 209  df-an 399  df-fo 6361

This theorem is referenced by:  dffo2  6594  foima  6595  fodmrnu  6598  f1imacnv  6631  foimacnv  6632  foun  6633  resdif  6635  fococnv2  6640  foelrni  6727  cbvfo  7045  isoini  7091  isofrlem  7093  isoselem  7094  canth  7111  f1opw2  7400  fornex  7657  wemoiso2  7675  curry1  7799  curry2  7802  bren  8518  en1  8576  fopwdom  8625  domss2  8676  mapen  8681  ssenen  8691  phplem4  8699  php3  8703  ssfi  8738  fodomfib  8798  f1opwfi  8828  ordiso2  8979  ordtypelem10  8991  oismo  9004  brwdom  9031  brwdom2  9037  wdomtr  9039  unxpwdom2  9052  wemapwe  9160  infxpenc2lem1  9445  fseqen  9453  fodomfi2  9486  infpwfien  9488  infmap2  9640  ackbij2  9665  infpssr  9730  fodomb  9948  fpwwe2lem6  10057  fpwwe2lem9  10060  tskuni  10205  gruen  10234  focdmex  13712  hashfacen  13813  supcvg  15211  ruclem13  15595  unbenlem  16244  imasval  16784  imasaddfnlem  16801  imasvscafn  16810  imasless  16813  xpsfrn  16841  fulloppc  17192  imasmnd2  17948  resgrpplusfrn  18117  imasgrp2  18214  oppglsm  18767  efgrelexlemb  18876  gsumzres  19029  gsumzcl2  19030  gsumzf1o  19032  gsumzaddlem  19041  gsumconst  19054  gsumzmhm  19057  gsumzoppg  19064  dprdf1o  19154  imasring  19369  gsumfsum  20612  zncyg  20695  znf1o  20698  znleval  20701  znunit  20710  cygznlem2a  20714  indlcim  20984  cmpfi  22016  cnconn  22030  1stcfb  22053  qtopval2  22304  basqtop  22319  tgqtop  22320  imastopn  22328  hmeontr  22377  hmeoqtop  22383  nrmhmph  22402  cmphaushmeo  22408  elfm3  22558  qustgpopn  22728  tsmsf1o  22753  imasf1oxmet  22985  imasf1omet  22986  imasf1oxms  23099  cnheiborlem  23558  ovolctb  24091  dyadmbl  24201  dvcnvrelem2  24615  dvcnvre  24616  efifo  25131  circgrp  25136  circsubm  25137  logrn  25142  dvrelog  25220  efopnlem2  25240  fsumdvdsmul  25772  f1otrg  26657  axcontlem10  26759  isgrpo  28274  isgrpoi  28275  pjrn  29484  padct  30455  cycpmconjvlem  30783  cycpmconjslem2  30797  imaslmod  30922  qusdimsum  31024  sigapildsys  31421  carsgclctunlem3  31578  ballotlemro  31780  erdsze2lem1  32450  cnpconn  32477  bdayimaon  33197  nosupbday  33205  noetalem3  33219  noetalem4  33220  bdayrn  33245  poimirlem15  34922  mblfinlem2  34945  volsupnfl  34952  ismtyres  35101  rngopidOLD  35146  opidon2OLD  35147  rngmgmbs4  35224  isgrpda  35248  mapdrn  38800  dnnumch2  39694  lnmlmic  39737  pwslnmlem1  39741  pwslnmlem2  39742  ntrneifv2  40479  ssnnf1octb  41505  stoweidlem27  42361  fourierdlem51  42491  fourierdlem102  42542  fourierdlem114  42554  sge0fodjrnlem  42747  nnfoctbdjlem  42786  nnfoctbdj  42787