MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  forn Structured version   Visualization version   GIF version

Theorem forn 6156
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
StepHypRef Expression
1 df-fo 5932 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
21simprbi 479 1 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  ran crn 5144   Fn wfn 5921  ontowfo 5924
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 197  df-an 385  df-fo 5932
This theorem is referenced by:  dffo2  6157  foima  6158  fodmrnu  6161  f1imacnv  6191  foimacnv  6192  foun  6193  resdif  6195  fococnv2  6200  foelrni  6283  cbvfo  6584  isoini  6628  isofrlem  6630  isoselem  6631  canth  6648  f1opw2  6930  fornex  7177  wemoiso2  7196  curry1  7314  curry2  7317  bren  8006  en1  8064  fopwdom  8109  domss2  8160  mapen  8165  ssenen  8175  phplem4  8183  php3  8187  ssfi  8221  fodomfib  8281  f1opwfi  8311  ordiso2  8461  ordtypelem10  8473  oismo  8486  brwdom  8513  brwdom2  8519  wdomtr  8521  unxpwdom2  8534  wemapwe  8632  infxpenc2lem1  8880  fseqen  8888  fodomfi2  8921  infpwfien  8923  infmap2  9078  ackbij2  9103  infpssr  9168  fodomb  9386  fpwwe2lem6  9495  fpwwe2lem9  9498  tskuni  9643  gruen  9672  focdmex  13179  hashfacen  13276  supcvg  14632  ruclem13  15015  unbenlem  15659  imasval  16218  imasaddfnlem  16235  imasvscafn  16244  imasless  16247  xpsfrn  16276  fulloppc  16629  imasmnd2  17374  resgrpplusfrn  17483  imasgrp2  17577  oppglsm  18103  efgrelexlemb  18209  gsumzres  18356  gsumzcl2  18357  gsumzf1o  18359  gsumzaddlem  18367  gsumconst  18380  gsumzmhm  18383  gsumzoppg  18390  dprdf1o  18477  imasring  18665  gsumfsum  19861  zncyg  19945  znf1o  19948  znleval  19951  znunit  19960  cygznlem2a  19964  indlcim  20227  cmpfi  21259  cnconn  21273  1stcfb  21296  qtopval2  21547  basqtop  21562  tgqtop  21563  imastopn  21571  hmeontr  21620  hmeoqtop  21626  nrmhmph  21645  cmphaushmeo  21651  elfm3  21801  qustgpopn  21970  tsmsf1o  21995  imasf1oxmet  22227  imasf1omet  22228  imasf1oxms  22341  cnheiborlem  22800  ovolctb  23304  dyadmbl  23414  dvcnvrelem2  23826  dvcnvre  23827  efifo  24338  circgrp  24343  circsubm  24344  logrn  24350  dvrelog  24428  efopnlem2  24448  fsumdvdsmul  24966  f1otrg  25796  axcontlem10  25898  isgrpo  27479  isgrpoi  27480  pjrn  28694  padct  29625  sigapildsys  30353  carsgclctunlem3  30510  ballotlemro  30712  erdsze2lem1  31311  cnpconn  31338  bdayimaon  31968  nosupbday  31976  noetalem3  31990  noetalem4  31991  bdayrn  32016  poimirlem15  33554  mblfinlem2  33577  volsupnfl  33584  ismtyres  33737  rngopidOLD  33782  opidon2OLD  33783  rngmgmbs4  33860  isgrpda  33884  mapdrn  37255  dnnumch2  37932  lnmlmic  37975  pwslnmlem1  37979  pwslnmlem2  37980  ntrneifv2  38695  ssnnf1octb  39696  stoweidlem27  40562  fourierdlem51  40692  fourierdlem102  40743  fourierdlem114  40755  sge0fodjrnlem  40951  nnfoctbdjlem  40990  nnfoctbdj  40991
  Copyright terms: Public domain W3C validator