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

Theorem f1ofo 6615
Description: A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.)
Assertion
Ref Expression
f1ofo (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)

Proof of Theorem f1ofo
StepHypRef Expression
1 dff1o3 6614 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
21simplbi 498 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  ccnv 5547  Fun wfun 6342  ontowfo 6346  1-1-ontowf1o 6347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355
This theorem is referenced by:  f1imacnv  6624  resin  6629  f1ococnv2  6634  fo00  6643  isoini  7080  isofrlem  7082  isoselem  7083  ncanth  7101  f1opw2  7389  f1dmex  7647  f1ovv  7648  f1oweALT  7662  wemoiso2  7664  curry1  7788  curry2  7791  smoiso2  7995  bren  8506  f1oeng  8516  en1  8564  canth2  8658  domss2  8664  mapen  8669  ssenen  8679  phplem4  8687  php3  8691  ssfi  8726  domunfican  8779  fiint  8783  f1fi  8799  f1opwfi  8816  mapfien  8859  supisolem  8925  ordiso2  8967  ordtypelem10  8979  oismo  8992  wdomref  9024  brwdom2  9025  unxpwdom2  9040  cantnflt2  9124  cantnfp1lem3  9131  wemapwe  9148  infxpenc2lem1  9433  fseqen  9441  infpwfien  9476  infmap2  9628  ackbij2  9653  cff1  9668  cofsmo  9679  infpssr  9718  enfin2i  9731  fin23lem27  9738  enfin1ai  9794  fin1a2lem7  9816  axcclem  9867  ttukeylem1  9919  fpwwe2lem6  10045  fpwwe2lem9  10048  canthp1lem2  10063  tskuni  10193  gruen  10222  cnexALT  12373  fiinfnf1o  13698  hasheqf1oi  13700  hashfacen  13800  fsumf1o  15068  fsumss  15070  fprodf1o  15288  fprodss  15290  ruc  15584  unbenlem  16232  xpsfrn  16829  xpsbas  16833  xpsadd  16835  xpsmul  16836  xpssca  16837  xpsvsca  16838  xpsless  16839  xpsle  16840  imasmndf1  17938  imasgrpf1  18154  gicsubgen  18356  symgmov2  18450  symgextfo  18479  symgfixelsi  18492  giccyg  18949  gsumzres  18958  gsumzcl2  18959  gsumzf1o  18961  gsumzaddlem  18970  gsumconst  18983  gsumzmhm  18986  gsumzoppg  18993  dprdf1o  19083  coe1mul2lem2  20364  gsumfsum  20540  znleval  20629  lmimlbs  20908  lbslcic  20913  cmpfi  21944  idqtop  22242  basqtop  22247  tgqtop  22248  hmeontr  22305  hmeoimaf1o  22306  hmeoqtop  22311  cmphmph  22324  connhmph  22325  nrmhmph  22330  indishmph  22334  cmphaushmeo  22336  xpstps  22346  xpstopnlem2  22347  fmid  22496  tsmsf1o  22680  imasdsf1olem  22910  imasf1oxmet  22912  imasf1omet  22913  xpsdsfn  22914  imasf1oxms  23026  imasf1oms  23027  iccpnfhmeo  23476  cnheiborlem  23485  ovolctb  24018  ovolicc2lem4  24048  dyadmbl  24128  mbfimaopnlem  24183  itg1addlem4  24227  dvcnvrelem2  24542  dvcnvre  24543  deg1ldg  24613  deg1leb  24616  efifo  25058  logrn  25069  dvrelog  25147  efopnlem2  25167  fsumdvdsmul  25699  f1otrg  26584  axcontlem10  26686  edgusgrnbfin  27082  eupthvdres  27941  cnvunop  29622  counop  29625  idunop  29682  elunop2  29717  fmptco1f1o  30306  padct  30381  symgcom  30654  cycpmconjvlem  30710  cycpmconjslem2  30724  xrge0iifiso  31077  volmeas  31389  ballotlemro  31679  derangenlem  32315  subfacp1lem3  32326  subfacp1lem5  32328  erdsze2lem1  32347  cvmsss2  32418  poimirlem1  34774  poimirlem2  34775  poimirlem3  34776  poimirlem4  34777  poimirlem5  34778  poimirlem6  34779  poimirlem7  34780  poimirlem9  34782  poimirlem10  34783  poimirlem11  34784  poimirlem12  34785  poimirlem14  34787  poimirlem15  34788  poimirlem16  34789  poimirlem17  34790  poimirlem19  34792  poimirlem20  34793  poimirlem22  34795  poimirlem23  34796  poimirlem24  34797  poimirlem25  34798  poimirlem29  34802  poimirlem31  34804  mblfinlem2  34811  ismtybndlem  34965  ismtyres  34967  diaintclN  38074  dibintclN  38183  mapdrn  38665  dnnumch2  39523  kelac1  39541  lnmlmic  39566  pwslnmlem1  39570  pwfi2f1o  39574  gicabl  39577  imasgim  39578  isnumbasgrplem1  39579  ntrneifv2  40308  stoweidlem27  42189  fourierdlem20  42289  fourierdlem51  42319  fourierdlem52  42320  fourierdlem63  42331  fourierdlem64  42332  fourierdlem65  42333  fourierdlem102  42370  fourierdlem114  42382  sge0f1o  42541  nnfoctbdjlem  42614  isomenndlem  42689  ovnsubaddlem1  42729  f1oresf1o2  43367  isomuspgrlem2d  43873  sursubmefmnd  43993
  Copyright terms: Public domain W3C validator