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

Theorem forn 6587
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 6355 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
21simprbi 497 1 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  ran crn 5550   Fn wfn 6344  ontowfo 6347
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 208  df-an 397  df-fo 6355
This theorem is referenced by:  dffo2  6588  foima  6589  fodmrnu  6592  f1imacnv  6625  foimacnv  6626  foun  6627  resdif  6629  fococnv2  6634  foelrni  6721  cbvfo  7036  isoini  7080  isofrlem  7082  isoselem  7083  canth  7100  f1opw2  7389  fornex  7648  wemoiso2  7666  curry1  7790  curry2  7793  bren  8507  en1  8565  fopwdom  8614  domss2  8665  mapen  8670  ssenen  8680  phplem4  8688  php3  8692  ssfi  8727  fodomfib  8787  f1opwfi  8817  ordiso2  8968  ordtypelem10  8980  oismo  8993  brwdom  9020  brwdom2  9026  wdomtr  9028  unxpwdom2  9041  wemapwe  9149  infxpenc2lem1  9434  fseqen  9442  fodomfi2  9475  infpwfien  9477  infmap2  9629  ackbij2  9654  infpssr  9719  fodomb  9937  fpwwe2lem6  10046  fpwwe2lem9  10049  tskuni  10194  gruen  10223  focdmex  13701  hashfacen  13802  supcvg  15201  ruclem13  15585  unbenlem  16234  imasval  16774  imasaddfnlem  16791  imasvscafn  16800  imasless  16803  xpsfrn  16831  fulloppc  17182  imasmnd2  17938  resgrpplusfrn  18057  imasgrp2  18154  oppglsm  18698  efgrelexlemb  18807  gsumzres  18960  gsumzcl2  18961  gsumzf1o  18963  gsumzaddlem  18972  gsumconst  18985  gsumzmhm  18988  gsumzoppg  18995  dprdf1o  19085  imasring  19300  gsumfsum  20542  zncyg  20625  znf1o  20628  znleval  20631  znunit  20640  cygznlem2a  20644  indlcim  20914  cmpfi  21946  cnconn  21960  1stcfb  21983  qtopval2  22234  basqtop  22249  tgqtop  22250  imastopn  22258  hmeontr  22307  hmeoqtop  22313  nrmhmph  22332  cmphaushmeo  22338  elfm3  22488  qustgpopn  22657  tsmsf1o  22682  imasf1oxmet  22914  imasf1omet  22915  imasf1oxms  23028  cnheiborlem  23487  ovolctb  24020  dyadmbl  24130  dvcnvrelem2  24544  dvcnvre  24545  efifo  25058  circgrp  25063  circsubm  25064  logrn  25069  dvrelog  25147  efopnlem2  25167  fsumdvdsmul  25700  f1otrg  26585  axcontlem10  26687  isgrpo  28202  isgrpoi  28203  pjrn  29412  padct  30382  cycpmconjvlem  30711  cycpmconjslem2  30725  imaslmod  30850  qusdimsum  30924  sigapildsys  31321  carsgclctunlem3  31478  ballotlemro  31680  erdsze2lem1  32348  cnpconn  32375  bdayimaon  33095  nosupbday  33103  noetalem3  33117  noetalem4  33118  bdayrn  33143  poimirlem15  34789  mblfinlem2  34812  volsupnfl  34819  ismtyres  34969  rngopidOLD  35014  opidon2OLD  35015  rngmgmbs4  35092  isgrpda  35116  mapdrn  38667  dnnumch2  39525  lnmlmic  39568  pwslnmlem1  39572  pwslnmlem2  39573  ntrneifv2  40310  ssnnf1octb  41336  stoweidlem27  42193  fourierdlem51  42323  fourierdlem102  42374  fourierdlem114  42386  sge0fodjrnlem  42579  nnfoctbdjlem  42618  nnfoctbdj  42619
  Copyright terms: Public domain W3C validator