Theorem f1ofo 6057

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

Step	Hyp	Ref	Expression
1		dff1o3 6056	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))
2	1	simplbi 475	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)

Syntax hints:   → wi 4  ^◡ccnv 5037  Fun wfun 5798  –onto→wfo 5802  –1-1-onto→wf1o 5803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811

This theorem is referenced by:  f1imacnv  6066  resin  6071  f1ococnv2  6076  fo00  6084  isoini  6488  isofrlem  6490  isoselem  6491  ncanth  6509  f1opw2  6786  f1dmex  7029  f1ovv  7030  f1oweALT  7043  wemoiso2  7045  curry1  7156  curry2  7159  smoiso2  7353  bren  7850  f1oeng  7860  en1  7909  canth2  7998  domss2  8004  mapen  8009  ssenen  8019  phplem4  8027  php3  8031  ssfi  8065  domunfican  8118  fiint  8122  f1fi  8136  f1opwfi  8153  mapfien  8196  supisolem  8262  ordiso2  8303  ordtypelem10  8315  oismo  8328  wdomref  8360  brwdom2  8361  unxpwdom2  8376  cantnflt2  8453  cantnfp1lem3  8460  wemapwe  8477  infxpenc2lem1  8725  fseqen  8733  infpwfien  8768  infmap2  8923  ackbij2  8948  cff1  8963  cofsmo  8974  infpssr  9013  enfin2i  9026  fin23lem27  9033  enfin1ai  9089  fin1a2lem7  9111  axcclem  9162  ttukeylem1  9214  fpwwe2lem6  9336  fpwwe2lem9  9339  canthp1lem2  9354  tskuni  9484  gruen  9513  cnexALT  11704  fiinfnf1o  13000  hasheqf1oi  13002  hashfacen  13095  fsumf1o  14301  fsumss  14303  fprodf1o  14515  fprodss  14517  ruc  14811  unbenlem  15450  xpsfrn  16052  xpsbas  16057  xpsadd  16059  xpsmul  16060  xpssca  16061  xpsvsca  16062  xpsless  16063  xpsle  16064  imasmndf1  17152  imasgrpf1  17355  gicsubgen  17544  symgmov2  17636  symgextfo  17665  symgfixelsi  17678  giccyg  18124  gsumzres  18133  gsumzcl2  18134  gsumzf1o  18136  gsumzaddlem  18144  gsumconst  18157  gsumzmhm  18160  gsumzoppg  18167  dprdf1o  18254  coe1mul2lem2  19459  gsumfsum  19632  znleval  19722  lmimlbs  19994  lbslcic  19999  cmpfi  21021  idqtop  21319  basqtop  21324  tgqtop  21325  hmeontr  21382  hmeoimaf1o  21383  hmeoqtop  21388  cmphmph  21401  conhmph  21402  nrmhmph  21407  indishmph  21411  cmphaushmeo  21413  xpstps  21423  xpstopnlem2  21424  fmid  21574  tsmsf1o  21758  imasdsf1olem  21988  imasf1oxmet  21990  imasf1omet  21991  xpsdsfn  21992  imasf1oxms  22104  imasf1oms  22105  iccpnfhmeo  22552  cnheiborlem  22561  ovolctb  23065  ovolicc2lem4  23095  dyadmbl  23174  mbfimaopnlem  23228  itg1addlem4  23272  dvcnvrelem2  23585  dvcnvre  23586  deg1ldg  23656  deg1leb  23659  efifo  24097  logrn  24109  dvrelog  24183  efopnlem2  24203  fsumdvdsmul  24721  f1otrg  25551  axcontlem10  25653  edgusgranbfin  25979  eupatrl  26495  eupares  26502  eupath2lem3  26506  eupath2  26507  cnvunop  28161  counop  28164  idunop  28221  elunop2  28256  padct  28885  xrge0iifiso  29309  volmeas  29621  ballotlemro  29911  derangenlem  30407  subfacp1lem3  30418  subfacp1lem5  30420  erdsze2lem1  30439  cvmsss2  30510  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem4  32583  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem9  32588  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem14  32593  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem22  32601  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem29  32608  poimirlem31  32610  mblfinlem2  32617  ismtybndlem  32775  ismtyres  32777  diaintclN  35365  dibintclN  35474  mapdrn  35956  dnnumch2  36633  kelac1  36651  lnmlmic  36676  pwslnmlem1  36680  pwfi2f1o  36684  gicabl  36687  imasgim  36688  isnumbasgrplem1  36690  ntrneifv2  37398  stoweidlem27  38920  fourierdlem20  39020  fourierdlem51  39050  fourierdlem52  39051  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem102  39101  fourierdlem114  39113  sge0f1o  39275  nnfoctbdjlem  39348  isomenndlem  39420  ovnsubaddlem1  39460  edgusgrnbfin  40601  eupthvdres  41403