Theorem f1ofo 5828

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

Assertion

Ref	Expression
f1ofo

Proof of Theorem f1ofo

Step	Hyp	Ref	Expression
1		dff1o3 5827	. 2
2	1	simplbi 460	1

Syntax hints:  ->wi 4  `'ccnv 5003  Funwfun 5587  -onto->wfo 5591  -1-1-onto->wf1o 5592

This theorem is referenced by:  f1imacnv  5837  resin  5842  f1ococnv2  5847  fo00  5854  isoini  6234  isofrlem  6236  isoselem  6237  ncanth  6255  f1opw2  6528  f1dmex  6770  f1ovv  6771  f1oweALT  6784  wemoiso2  6786  curry1  6892  curry2  6895  smoiso2  7059  bren  7545  f1oeng  7554  en1  7602  canth2  7690  domss2  7696  mapen  7701  ssenen  7711  phplem4  7719  php3  7723  ssfi  7760  domunfican  7813  fiint  7817  f1fi  7827  f1opwfi  7844  mapfien  7887  supisolem  7952  ordiso2  7961  ordtypelem10  7973  oismo  7986  wdomref  8019  brwdom2  8020  unxpwdom2  8035  cantnflt2  8113  cantnfp1lem3  8120  cantnflt2OLD  8143  cantnfp1lem3OLD  8146  mapfienOLD  8159  wemapwe  8160  wemapweOLD  8161  infxpenc2lem1  8417  fseqen  8429  infpwfien  8464  infmap2  8619  ackbij2  8644  cff1  8659  cofsmo  8670  infpssr  8709  enfin2i  8722  fin23lem27  8729  enfin1ai  8785  fin1a2lem7  8807  axcclem  8858  ttukeylem1  8910  fpwwe2lem6  9034  fpwwe2lem9  9037  canthp1lem2  9052  tskuni  9182  gruen  9211  cnexALT  11245  1fv  11821  fiinfnf1o  12423  hashfacen  12503  fsumf1o  13545  fsumss  13547  fprodf1o  13753  fprodss  13755  ruc  13976  unbenlem  14426  xpsfrn  14966  xpsbas  14971  xpsadd  14973  xpsmul  14974  xpssca  14975  xpsvsca  14976  xpsless  14977  xpsle  14978  imasmndf1  15959  imasgrpf1  16187  gicsubgen  16326  symgmov2  16418  symgextfo  16447  symgfixelsi  16460  giccyg  16902  gsumval3OLD  16908  gsumzres  16914  gsumzcl2  16915  gsumzf1o  16917  gsumzresOLD  16918  gsumzclOLD  16919  gsumzf1oOLD  16920  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsumconst  16954  gsumzmhm  16957  gsumzmhmOLD  16958  gsumzoppg  16967  gsumzoppgOLD  16968  dprdf1o  17079  coe1mul2lem2  18309  gsumfsum  18484  znleval  18593  lmimlbs  18871  lbslcic  18876  cmpfi  19908  idqtop  20207  basqtop  20212  tgqtop  20213  hmeontr  20270  hmeoimaf1o  20271  hmeoqtop  20276  cmphmph  20289  conhmph  20290  nrmhmph  20295  indishmph  20299  cmphaushmeo  20301  xpstps  20311  xpstopnlem2  20312  fmid  20461  tsmsf1o  20647  imasdsf1olem  20876  imasf1oxmet  20878  imasf1omet  20879  xpsdsfn  20880  imasf1oxms  20992  imasf1oms  20993  iccpnfhmeo  21445  cnheiborlem  21454  ovolctb  21901  ovolicc2lem4  21931  dyadmbl  22009  mbfimaopnlem  22062  itg1addlem4  22106  dvcnvrelem2  22419  dvcnvre  22420  deg1ldg  22492  deg1leb  22495  efifo  22934  logrn  22946  dvrelog  23018  efopnlem2  23038  fsumdvdsmul  23471  f1otrg  24174  axcontlem10  24276  edgusgranbfin  24450  eupatrl  24968  eupares  24975  eupath2lem3  24979  eupath2  24980  cnvunop  26837  counop  26840  idunop  26897  elunop2  26932  xrge0iifiso  27917  volmeas  28203  ballotlemro  28461  derangenlem  28615  subfacp1lem3  28626  subfacp1lem5  28628  erdsze2lem1  28647  cvmsss2  28719  mblfinlem2  30052  ismtybndlem  30302  ismtyres  30304  dnnumch2  30991  kelac1  31009  lnmlmic  31034  pwslnmlem1  31038  pwfi2f1o  31044  gicabl  31047  imasgim  31048  isnumbasgrplem1  31050  stoweidlem27  31809  fourierdlem20  31909  fourierdlem51  31940  fourierdlem52  31941  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem102  31991  fourierdlem114  32003  bj-finsumval0  34663  diaintclN  36785  dibintclN  36894  mapdrn  37376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600