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

Theorem f1ofo 6182
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 6181 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
21simplbi 475 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  ccnv 5142  Fun wfun 5920  ontowfo 5924  1-1-ontowf1o 5925
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933
This theorem is referenced by:  f1imacnv  6191  resin  6196  f1ococnv2  6201  fo00  6210  isoini  6628  isofrlem  6630  isoselem  6631  ncanth  6649  f1opw2  6930  f1dmex  7178  f1ovv  7179  f1oweALT  7194  wemoiso2  7196  curry1  7314  curry2  7317  smoiso2  7511  bren  8006  f1oeng  8016  en1  8064  canth2  8154  domss2  8160  mapen  8165  ssenen  8175  phplem4  8183  php3  8187  ssfi  8221  domunfican  8274  fiint  8278  f1fi  8294  f1opwfi  8311  mapfien  8354  supisolem  8420  ordiso2  8461  ordtypelem10  8473  oismo  8486  wdomref  8518  brwdom2  8519  unxpwdom2  8534  cantnflt2  8608  cantnfp1lem3  8615  wemapwe  8632  infxpenc2lem1  8880  fseqen  8888  infpwfien  8923  infmap2  9078  ackbij2  9103  cff1  9118  cofsmo  9129  infpssr  9168  enfin2i  9181  fin23lem27  9188  enfin1ai  9244  fin1a2lem7  9266  axcclem  9317  ttukeylem1  9369  fpwwe2lem6  9495  fpwwe2lem9  9498  canthp1lem2  9513  tskuni  9643  gruen  9672  cnexALT  11866  fiinfnf1o  13178  hasheqf1oi  13180  hashfacen  13276  fsumf1o  14498  fsumss  14500  fprodf1o  14720  fprodss  14722  ruc  15016  unbenlem  15659  xpsfrn  16276  xpsbas  16281  xpsadd  16283  xpsmul  16284  xpssca  16285  xpsvsca  16286  xpsless  16287  xpsle  16288  imasmndf1  17376  imasgrpf1  17579  gicsubgen  17767  symgmov2  17859  symgextfo  17888  symgfixelsi  17901  giccyg  18347  gsumzres  18356  gsumzcl2  18357  gsumzf1o  18359  gsumzaddlem  18367  gsumconst  18380  gsumzmhm  18383  gsumzoppg  18390  dprdf1o  18477  coe1mul2lem2  19686  gsumfsum  19861  znleval  19951  lmimlbs  20223  lbslcic  20228  cmpfi  21259  idqtop  21557  basqtop  21562  tgqtop  21563  hmeontr  21620  hmeoimaf1o  21621  hmeoqtop  21626  cmphmph  21639  connhmph  21640  nrmhmph  21645  indishmph  21649  cmphaushmeo  21651  xpstps  21661  xpstopnlem2  21662  fmid  21811  tsmsf1o  21995  imasdsf1olem  22225  imasf1oxmet  22227  imasf1omet  22228  xpsdsfn  22229  imasf1oxms  22341  imasf1oms  22342  iccpnfhmeo  22791  cnheiborlem  22800  ovolctb  23304  ovolicc2lem4  23334  dyadmbl  23414  mbfimaopnlem  23467  itg1addlem4  23511  dvcnvrelem2  23826  dvcnvre  23827  deg1ldg  23897  deg1leb  23900  efifo  24338  logrn  24350  dvrelog  24428  efopnlem2  24448  fsumdvdsmul  24966  f1otrg  25796  axcontlem10  25898  edgusgrnbfin  26319  eupthvdres  27213  cnvunop  28905  counop  28908  idunop  28965  elunop2  29000  fmptco1f1o  29562  padct  29625  xrge0iifiso  30109  volmeas  30422  ballotlemro  30712  derangenlem  31279  subfacp1lem3  31290  subfacp1lem5  31292  erdsze2lem1  31311  cvmsss2  31382  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem4  33543  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem9  33548  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem14  33553  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem22  33561  poimirlem23  33562  poimirlem24  33563  poimirlem25  33564  poimirlem29  33568  poimirlem31  33570  mblfinlem2  33577  ismtybndlem  33735  ismtyres  33737  diaintclN  36664  dibintclN  36773  mapdrn  37255  dnnumch2  37932  kelac1  37950  lnmlmic  37975  pwslnmlem1  37979  pwfi2f1o  37983  gicabl  37986  imasgim  37987  isnumbasgrplem1  37988  ntrneifv2  38695  stoweidlem27  40562  fourierdlem20  40662  fourierdlem51  40692  fourierdlem52  40693  fourierdlem63  40704  fourierdlem64  40705  fourierdlem65  40706  fourierdlem102  40743  fourierdlem114  40755  sge0f1o  40917  nnfoctbdjlem  40990  isomenndlem  41065  ovnsubaddlem1  41105
  Copyright terms: Public domain W3C validator