Theorem f1ofo 6144

Description: A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.)

Assertion

Ref	Expression
f1ofo	|- ( F : A -1-1-onto-> B -> F : A -onto-> B )

Proof of Theorem f1ofo

Step	Hyp	Ref	Expression
1		dff1o3 6143	. 2 |- ( F : A -1-1-onto-> B <-> ( F : A -onto-> B /\ Fun `' F ) )
2	1	simplbi 476	1 |- ( F : A -1-1-onto-> B -> F : A -onto-> B )

Syntax hints:   -> wi 4   `'ccnv 5113   Fun wfun 5882   -onto->wfo 5886   -1-1-onto->wf1o 5887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895

This theorem is referenced by:  f1imacnv  6153  resin  6158  f1ococnv2  6163  fo00  6172  isoini  6588  isofrlem  6590  isoselem  6591  ncanth  6609  f1opw2  6888  f1dmex  7136  f1ovv  7137  f1oweALT  7152  wemoiso2  7154  curry1  7269  curry2  7272  smoiso2  7466  bren  7964  f1oeng  7974  en1  8023  canth2  8113  domss2  8119  mapen  8124  ssenen  8134  phplem4  8142  php3  8146  ssfi  8180  domunfican  8233  fiint  8237  f1fi  8253  f1opwfi  8270  mapfien  8313  supisolem  8379  ordiso2  8420  ordtypelem10  8432  oismo  8445  wdomref  8477  brwdom2  8478  unxpwdom2  8493  cantnflt2  8570  cantnfp1lem3  8577  wemapwe  8594  infxpenc2lem1  8842  fseqen  8850  infpwfien  8885  infmap2  9040  ackbij2  9065  cff1  9080  cofsmo  9091  infpssr  9130  enfin2i  9143  fin23lem27  9150  enfin1ai  9206  fin1a2lem7  9228  axcclem  9279  ttukeylem1  9331  fpwwe2lem6  9457  fpwwe2lem9  9460  canthp1lem2  9475  tskuni  9605  gruen  9634  cnexALT  11828  fiinfnf1o  13138  hasheqf1oi  13140  hashfacen  13238  fsumf1o  14454  fsumss  14456  fprodf1o  14676  fprodss  14678  ruc  14972  unbenlem  15612  xpsfrn  16229  xpsbas  16234  xpsadd  16236  xpsmul  16237  xpssca  16238  xpsvsca  16239  xpsless  16240  xpsle  16241  imasmndf1  17329  imasgrpf1  17532  gicsubgen  17721  symgmov2  17813  symgextfo  17842  symgfixelsi  17855  giccyg  18301  gsumzres  18310  gsumzcl2  18311  gsumzf1o  18313  gsumzaddlem  18321  gsumconst  18334  gsumzmhm  18337  gsumzoppg  18344  dprdf1o  18431  coe1mul2lem2  19638  gsumfsum  19813  znleval  19903  lmimlbs  20175  lbslcic  20180  cmpfi  21211  idqtop  21509  basqtop  21514  tgqtop  21515  hmeontr  21572  hmeoimaf1o  21573  hmeoqtop  21578  cmphmph  21591  connhmph  21592  nrmhmph  21597  indishmph  21601  cmphaushmeo  21603  xpstps  21613  xpstopnlem2  21614  fmid  21764  tsmsf1o  21948  imasdsf1olem  22178  imasf1oxmet  22180  imasf1omet  22181  xpsdsfn  22182  imasf1oxms  22294  imasf1oms  22295  iccpnfhmeo  22744  cnheiborlem  22753  ovolctb  23258  ovolicc2lem4  23288  dyadmbl  23368  mbfimaopnlem  23422  itg1addlem4  23466  dvcnvrelem2  23781  dvcnvre  23782  deg1ldg  23852  deg1leb  23855  efifo  24293  logrn  24305  dvrelog  24383  efopnlem2  24403  fsumdvdsmul  24921  f1otrg  25751  axcontlem10  25853  edgusgrnbfin  26275  eupthvdres  27095  cnvunop  28777  counop  28780  idunop  28837  elunop2  28872  fmptco1f1o  29434  padct  29497  xrge0iifiso  29981  volmeas  30294  ballotlemro  30584  derangenlem  31153  subfacp1lem3  31164  subfacp1lem5  31166  erdsze2lem1  31185  cvmsss2  31256  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem9  33418  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem29  33438  poimirlem31  33440  mblfinlem2  33447  ismtybndlem  33605  ismtyres  33607  diaintclN  36347  dibintclN  36456  mapdrn  36938  dnnumch2  37615  kelac1  37633  lnmlmic  37658  pwslnmlem1  37662  pwfi2f1o  37666  gicabl  37669  imasgim  37670  isnumbasgrplem1  37671  ntrneifv2  38378  stoweidlem27  40244  fourierdlem20  40344  fourierdlem51  40374  fourierdlem52  40375  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem102  40425  fourierdlem114  40437  sge0f1o  40599  nnfoctbdjlem  40672  isomenndlem  40744  ovnsubaddlem1  40784