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

Theorem forn 6031
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 5810 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
21simprbi 479 1 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  ran crn 5039   Fn wfn 5799  ontowfo 5802
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 196  df-an 385  df-fo 5810
This theorem is referenced by:  dffo2  6032  foima  6033  fodmrnu  6036  f1imacnv  6066  foimacnv  6067  foun  6068  resdif  6070  fococnv2  6075  foelrni  6154  cbvfo  6444  isoini  6488  isofrlem  6490  isoselem  6491  canth  6508  f1opw2  6786  fornex  7028  wemoiso2  7045  curry1  7156  curry2  7159  bren  7850  en1  7909  fopwdom  7953  domss2  8004  mapen  8009  ssenen  8019  phplem4  8027  php3  8031  ssfi  8065  fodomfib  8125  f1opwfi  8153  ordiso2  8303  ordtypelem10  8315  oismo  8328  brwdom  8355  brwdom2  8361  wdomtr  8363  unxpwdom2  8376  wemapwe  8477  infxpenc2lem1  8725  fseqen  8733  fodomfi2  8766  infpwfien  8768  infmap2  8923  ackbij2  8948  infpssr  9013  fodomb  9229  fpwwe2lem6  9336  fpwwe2lem9  9339  tskuni  9484  gruen  9513  focdmex  13001  hashfacen  13095  supcvg  14427  ruclem13  14810  unbenlem  15450  imasval  15994  imasaddfnlem  16011  imasvscafn  16020  imasless  16023  xpsfrn  16052  fulloppc  16405  imasmnd2  17150  resgrpplusfrn  17259  imasgrp2  17353  oppglsm  17880  efgrelexlemb  17986  gsumzres  18133  gsumzcl2  18134  gsumzf1o  18136  gsumzaddlem  18144  gsumconst  18157  gsumzmhm  18160  gsumzoppg  18167  dprdf1o  18254  imasring  18442  gsumfsum  19632  zncyg  19716  znf1o  19719  znleval  19722  znunit  19731  cygznlem2a  19735  indlcim  19998  cmpfi  21021  cnconn  21035  1stcfb  21058  qtopval2  21309  basqtop  21324  tgqtop  21325  imastopn  21333  hmeontr  21382  hmeoqtop  21388  nrmhmph  21407  cmphaushmeo  21413  elfm3  21564  qustgpopn  21733  tsmsf1o  21758  imasf1oxmet  21990  imasf1omet  21991  imasf1oxms  22104  cnheiborlem  22561  ovolctb  23065  dyadmbl  23174  dvcnvrelem2  23585  dvcnvre  23586  efifo  24097  circgrp  24102  circsubm  24103  logrn  24109  dvrelog  24183  efopnlem2  24203  fsumdvdsmul  24721  f1otrg  25551  axcontlem10  25653  eupares  26502  eupath2lem3  26506  isgrpo  26735  isgrpoi  26736  pjrn  27950  padct  28885  sigapildsys  29552  carsgclctunlem3  29709  ballotlemro  29911  erdsze2lem1  30439  cnpcon  30466  bdayrn  31076  poimirlem15  32594  mblfinlem2  32617  volsupnfl  32624  ismtyres  32777  rngopidOLD  32822  opidon2OLD  32823  rngmgmbs4  32900  isgrpda  32924  mapdrn  35956  dnnumch2  36633  lnmlmic  36676  pwslnmlem1  36680  pwslnmlem2  36681  ntrneifv2  37398  ssnnf1octb  38377  stoweidlem27  38920  fourierdlem51  39050  fourierdlem102  39101  fourierdlem114  39113  sge0fodjrnlem  39309  nnfoctbdjlem  39348  nnfoctbdj  39349
  Copyright terms: Public domain W3C validator