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

Theorem f1ofo 6616
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 6615 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
21simplbi 498 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  ccnv 5548  Fun wfun 6343  ontowfo 6347  1-1-ontowf1o 6348
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 2793
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 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356
This theorem is referenced by:  f1imacnv  6625  resin  6630  f1ococnv2  6635  fo00  6644  isoini  7080  isofrlem  7082  isoselem  7083  ncanth  7101  f1opw2  7389  f1dmex  7649  f1ovv  7650  f1oweALT  7664  wemoiso2  7666  curry1  7790  curry2  7793  smoiso2  7997  bren  8507  f1oeng  8517  en1  8565  canth2  8659  domss2  8665  mapen  8670  ssenen  8680  phplem4  8688  php3  8692  ssfi  8727  domunfican  8780  fiint  8784  f1fi  8800  f1opwfi  8817  mapfien  8860  supisolem  8926  ordiso2  8968  ordtypelem10  8980  oismo  8993  wdomref  9025  brwdom2  9026  unxpwdom2  9041  cantnflt2  9125  cantnfp1lem3  9132  wemapwe  9149  infxpenc2lem1  9434  fseqen  9442  infpwfien  9477  infmap2  9629  ackbij2  9654  cff1  9669  cofsmo  9680  infpssr  9719  enfin2i  9732  fin23lem27  9739  enfin1ai  9795  fin1a2lem7  9817  axcclem  9868  ttukeylem1  9920  fpwwe2lem6  10046  fpwwe2lem9  10049  canthp1lem2  10064  tskuni  10194  gruen  10223  cnexALT  12375  fiinfnf1o  13700  hasheqf1oi  13702  hashfacen  13802  fsumf1o  15070  fsumss  15072  fprodf1o  15290  fprodss  15292  ruc  15586  unbenlem  16234  xpsfrn  16831  xpsbas  16835  xpsadd  16837  xpsmul  16838  xpssca  16839  xpsvsca  16840  xpsless  16841  xpsle  16842  imasmndf1  17940  imasgrpf1  18156  gicsubgen  18358  symgmov2  18452  symgextfo  18481  symgfixelsi  18494  giccyg  18951  gsumzres  18960  gsumzcl2  18961  gsumzf1o  18963  gsumzaddlem  18972  gsumconst  18985  gsumzmhm  18988  gsumzoppg  18995  dprdf1o  19085  coe1mul2lem2  20366  gsumfsum  20542  znleval  20631  lmimlbs  20910  lbslcic  20915  cmpfi  21946  idqtop  22244  basqtop  22249  tgqtop  22250  hmeontr  22307  hmeoimaf1o  22308  hmeoqtop  22313  cmphmph  22326  connhmph  22327  nrmhmph  22332  indishmph  22336  cmphaushmeo  22338  xpstps  22348  xpstopnlem2  22349  fmid  22498  tsmsf1o  22682  imasdsf1olem  22912  imasf1oxmet  22914  imasf1omet  22915  xpsdsfn  22916  imasf1oxms  23028  imasf1oms  23029  iccpnfhmeo  23478  cnheiborlem  23487  ovolctb  24020  ovolicc2lem4  24050  dyadmbl  24130  mbfimaopnlem  24185  itg1addlem4  24229  dvcnvrelem2  24544  dvcnvre  24545  deg1ldg  24615  deg1leb  24618  efifo  25058  logrn  25069  dvrelog  25147  efopnlem2  25167  fsumdvdsmul  25700  f1otrg  26585  axcontlem10  26687  edgusgrnbfin  27083  eupthvdres  27942  cnvunop  29623  counop  29626  idunop  29683  elunop2  29718  fmptco1f1o  30307  padct  30382  symgcom  30655  cycpmconjvlem  30711  cycpmconjslem2  30725  xrge0iifiso  31078  volmeas  31390  ballotlemro  31680  derangenlem  32316  subfacp1lem3  32327  subfacp1lem5  32329  erdsze2lem1  32348  cvmsss2  32419  poimirlem1  34775  poimirlem2  34776  poimirlem3  34777  poimirlem4  34778  poimirlem5  34779  poimirlem6  34780  poimirlem7  34781  poimirlem9  34783  poimirlem10  34784  poimirlem11  34785  poimirlem12  34786  poimirlem14  34788  poimirlem15  34789  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem22  34796  poimirlem23  34797  poimirlem24  34798  poimirlem25  34799  poimirlem29  34803  poimirlem31  34805  mblfinlem2  34812  ismtybndlem  34967  ismtyres  34969  diaintclN  38076  dibintclN  38185  mapdrn  38667  dnnumch2  39525  kelac1  39543  lnmlmic  39568  pwslnmlem1  39572  pwfi2f1o  39576  gicabl  39579  imasgim  39580  isnumbasgrplem1  39581  ntrneifv2  40310  stoweidlem27  42193  fourierdlem20  42293  fourierdlem51  42323  fourierdlem52  42324  fourierdlem63  42335  fourierdlem64  42336  fourierdlem65  42337  fourierdlem102  42374  fourierdlem114  42386  sge0f1o  42545  nnfoctbdjlem  42618  isomenndlem  42693  ovnsubaddlem1  42733  f1oresf1o2  43371  isomuspgrlem2d  43843  sursubmefmnd  43963
  Copyright terms: Public domain W3C validator