Theorem f1ofo 6624

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 6623	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))
2	1	simplbi 500	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)

Syntax hints:   → wi 4  ^◡ccnv 5556  Fun wfun 6351  –onto→wfo 6355  –1-1-onto→wf1o 6356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364

This theorem is referenced by:  f1imacnv  6633  resin  6638  f1ococnv2  6643  fo00  6652  isoini  7093  isofrlem  7095  isoselem  7096  ncanth  7114  f1opw2  7402  f1dmex  7660  f1ovv  7661  f1oweALT  7675  wemoiso2  7677  curry1  7801  curry2  7804  smoiso2  8008  bren  8520  f1oeng  8530  en1  8578  canth2  8672  domss2  8678  mapen  8683  ssenen  8693  phplem4  8701  php3  8705  ssfi  8740  domunfican  8793  fiint  8797  f1fi  8813  f1opwfi  8830  mapfien  8873  supisolem  8939  ordiso2  8981  ordtypelem10  8993  oismo  9006  wdomref  9038  brwdom2  9039  unxpwdom2  9054  cantnflt2  9138  cantnfp1lem3  9145  wemapwe  9162  infxpenc2lem1  9447  fseqen  9455  infpwfien  9490  infmap2  9642  ackbij2  9667  cff1  9682  cofsmo  9693  infpssr  9732  enfin2i  9745  fin23lem27  9752  enfin1ai  9808  fin1a2lem7  9830  axcclem  9881  ttukeylem1  9933  fpwwe2lem6  10059  fpwwe2lem9  10062  canthp1lem2  10077  tskuni  10207  gruen  10236  cnexALT  12388  fiinfnf1o  13713  hasheqf1oi  13715  hashfacen  13815  fsumf1o  15082  fsumss  15084  fprodf1o  15302  fprodss  15304  ruc  15598  unbenlem  16246  xpsfrn  16843  xpsbas  16847  xpsadd  16849  xpsmul  16850  xpssca  16851  xpsvsca  16852  xpsless  16853  xpsle  16854  imasmndf1  17952  sursubmefmnd  18063  imasgrpf1  18218  gicsubgen  18420  symgmov2  18518  symgextfo  18552  symgfixelsi  18565  giccyg  19022  gsumzres  19031  gsumzcl2  19032  gsumzf1o  19034  gsumzaddlem  19043  gsumconst  19056  gsumzmhm  19059  gsumzoppg  19066  dprdf1o  19156  coe1mul2lem2  20438  gsumfsum  20614  znleval  20703  lmimlbs  20982  lbslcic  20987  cmpfi  22018  idqtop  22316  basqtop  22321  tgqtop  22322  hmeontr  22379  hmeoimaf1o  22380  hmeoqtop  22385  cmphmph  22398  connhmph  22399  nrmhmph  22404  indishmph  22408  cmphaushmeo  22410  xpstps  22420  xpstopnlem2  22421  fmid  22570  tsmsf1o  22755  imasdsf1olem  22985  imasf1oxmet  22987  imasf1omet  22988  xpsdsfn  22989  imasf1oxms  23101  imasf1oms  23102  iccpnfhmeo  23551  cnheiborlem  23560  ovolctb  24093  ovolicc2lem4  24123  dyadmbl  24203  mbfimaopnlem  24258  itg1addlem4  24302  dvcnvrelem2  24617  dvcnvre  24618  deg1ldg  24688  deg1leb  24691  efifo  25133  logrn  25144  dvrelog  25222  efopnlem2  25242  fsumdvdsmul  25774  f1otrg  26659  axcontlem10  26761  edgusgrnbfin  27157  eupthvdres  28016  cnvunop  29697  counop  29700  idunop  29757  elunop2  29792  fmptco1f1o  30380  padct  30457  symgcom  30729  cycpmconjvlem  30785  cycpmconjslem2  30799  xrge0iifiso  31180  volmeas  31492  ballotlemro  31782  derangenlem  32420  subfacp1lem3  32431  subfacp1lem5  32433  erdsze2lem1  32452  cvmsss2  32523  poimirlem1  34895  poimirlem2  34896  poimirlem3  34897  poimirlem4  34898  poimirlem5  34899  poimirlem6  34900  poimirlem7  34901  poimirlem9  34903  poimirlem10  34904  poimirlem11  34905  poimirlem12  34906  poimirlem14  34908  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem22  34916  poimirlem23  34917  poimirlem24  34918  poimirlem25  34919  poimirlem29  34923  poimirlem31  34925  mblfinlem2  34932  ismtybndlem  35086  ismtyres  35088  diaintclN  38196  dibintclN  38305  mapdrn  38787  dnnumch2  39652  kelac1  39670  lnmlmic  39695  pwslnmlem1  39699  pwfi2f1o  39703  gicabl  39706  imasgim  39707  isnumbasgrplem1  39708  ntrneifv2  40437  stoweidlem27  42319  fourierdlem20  42419  fourierdlem51  42449  fourierdlem52  42450  fourierdlem63  42461  fourierdlem64  42462  fourierdlem65  42463  fourierdlem102  42500  fourierdlem114  42512  sge0f1o  42671  nnfoctbdjlem  42744  isomenndlem  42819  ovnsubaddlem1  42859  f1oresf1o2  43497  isomuspgrlem2d  44003