Theorem f1ofo 6869

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

Syntax hints:   → wi 4  ^◡ccnv 5699  Fun wfun 6567  –onto→wfo 6571  –1-1-onto→wf1o 6572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1778  df-cleq 2732  df-ss 3993  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580

This theorem is referenced by:  f1imacnv  6878  resin  6884  f1ococnv2  6889  fo00  6898  f1ocoima  7339  isoini  7374  isofrlem  7376  isoselem  7377  ncanth  7402  f1opw2  7705  f1dmex  7997  f1ovv  7998  f1oweALT  8013  wemoiso2  8015  mptcnfimad  8027  curry1  8145  curry2  8148  smoiso2  8425  f1osetex  8917  bren  9013  brenOLD  9014  f1oeng  9031  en1  9086  en1OLD  9087  canth2  9196  domss2  9202  mapen  9207  ssenen  9217  dif1enlem  9222  dif1enlemOLD  9223  ssfiALT  9241  phplem2  9271  php3  9275  phplem4OLD  9283  php3OLD  9287  f1fi  9380  domunfican  9389  fiint  9394  fiintOLD  9395  f1opwfi  9426  mapfien  9477  supisolem  9542  ordiso2  9584  ordtypelem10  9596  oismo  9609  wdomref  9641  brwdom2  9642  unxpwdom2  9657  cantnflt2  9742  cantnfp1lem3  9749  wemapwe  9766  infxpenc2lem1  10088  fseqen  10096  infpwfien  10131  infmap2  10286  ackbij2  10311  cff1  10327  cofsmo  10338  infpssr  10377  enfin2i  10390  fin23lem27  10397  enfin1ai  10453  fin1a2lem7  10475  axcclem  10526  ttukeylem1  10578  fpwwe2lem5  10704  fpwwe2lem8  10707  canthp1lem2  10722  tskuni  10852  gruen  10881  cnexALT  13051  fiinfnf1o  14399  hasheqf1oi  14400  hashfacen  14503  fsumf1o  15771  fsumss  15773  fprodf1o  15994  fprodss  15996  ruc  16291  unbenlem  16955  xpsfrn  17628  xpsbas  17632  xpsadd  17634  xpsmul  17635  xpssca  17636  xpsvsca  17637  xpsless  17638  xpsle  17639  imasmndf1  18811  sursubmefmnd  18931  imasgrpf1  19097  gicsubgen  19319  symgmov2  19429  symgextfo  19464  symgfixelsi  19477  giccyg  19942  gsumzres  19951  gsumzcl2  19952  gsumzf1o  19954  gsumzaddlem  19963  gsumconst  19976  gsumzmhm  19979  gsumzoppg  19986  dprdf1o  20076  imasrngf1  20205  imasringf1  20354  gsumfsum  21475  znleval  21596  lmimlbs  21879  lbslcic  21884  coe1mul2lem2  22292  cmpfi  23437  idqtop  23735  basqtop  23740  tgqtop  23741  hmeontr  23798  hmeoimaf1o  23799  hmeoqtop  23804  cmphmph  23817  connhmph  23818  nrmhmph  23823  indishmph  23827  cmphaushmeo  23829  xpstps  23839  xpstopnlem2  23840  fmid  23989  tsmsf1o  24174  imasdsf1olem  24404  imasf1oxmet  24406  imasf1omet  24407  xpsdsfn  24408  imasf1oxms  24523  imasf1oms  24524  iccpnfhmeo  24995  cnheiborlem  25005  ovolctb  25544  ovolicc2lem4  25574  dyadmbl  25654  mbfimaopnlem  25709  itg1addlem4  25753  itg1addlem4OLD  25754  dvcnvrelem2  26077  dvcnvre  26078  deg1ldg  26151  deg1leb  26154  efifo  26607  logrn  26618  dvrelog  26697  efopnlem2  26717  fsumdvdsmul  27256  fsumdvdsmulOLD  27258  f1otrg  28897  axcontlem10  29006  edgusgrnbfin  29408  eupthvdres  30267  cnvunop  31950  counop  31953  idunop  32010  elunop2  32045  fmptco1f1o  32652  padct  32733  mndlactf1o  33016  mndractf1o  33017  symgcom  33076  cycpmconjvlem  33134  cycpmconjslem2  33148  1arithidomlem2  33529  xrge0iifiso  33881  volmeas  34195  ballotlemro  34487  derangenlem  35139  subfacp1lem3  35150  subfacp1lem5  35152  erdsze2lem1  35171  cvmsss2  35242  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem9  37589  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem14  37594  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem29  37609  poimirlem31  37611  mblfinlem2  37618  ismtybndlem  37766  ismtyres  37768  diaintclN  41015  dibintclN  41124  mapdrn  41606  aks6d1c1p5  42069  riccrng1  42476  ricdrng1  42483  dnnumch2  43002  kelac1  43020  lnmlmic  43045  pwslnmlem1  43049  pwfi2f1o  43053  gicabl  43056  imasgim  43057  isnumbasgrplem1  43058  ntrneifv2  44042  stoweidlem27  45948  fourierdlem20  46048  fourierdlem51  46078  fourierdlem52  46079  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem102  46129  fourierdlem114  46141  sge0f1o  46303  nnfoctbdjlem  46376  isomenndlem  46451  ovnsubaddlem1  46491  3f1oss1  46990  f1oresf1o2  47206  uspgrimprop  47757  isuspgrimlem  47758  grimuhgr  47762  grimcnv  47763  grimedg  47787