Theorem f1ofo 6732

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

Syntax hints:   → wi 4  ^◡ccnv 5589  Fun wfun 6431  –onto→wfo 6435  –1-1-onto→wf1o 6436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444

This theorem is referenced by:  f1imacnv  6741  resin  6747  f1ococnv2  6752  fo00  6761  isoini  7218  isofrlem  7220  isoselem  7221  ncanth  7239  f1opw2  7533  f1dmex  7808  f1ovv  7809  f1oweALT  7824  wemoiso2  7826  curry1  7953  curry2  7956  smoiso2  8209  f1osetex  8656  bren  8752  brenOLD  8753  f1oeng  8768  en1  8820  en1OLD  8821  canth2  8926  domss2  8932  mapen  8937  ssenen  8947  dif1enlem  8952  ssfiALT  8966  phplem2  9000  php3  9004  phplem4OLD  9012  php3OLD  9016  domunfican  9096  fiint  9100  f1fi  9115  f1opwfi  9132  mapfien  9176  supisolem  9241  ordiso2  9283  ordtypelem10  9295  oismo  9308  wdomref  9340  brwdom2  9341  unxpwdom2  9356  cantnflt2  9440  cantnfp1lem3  9447  wemapwe  9464  infxpenc2lem1  9784  fseqen  9792  infpwfien  9827  infmap2  9983  ackbij2  10008  cff1  10023  cofsmo  10034  infpssr  10073  enfin2i  10086  fin23lem27  10093  enfin1ai  10149  fin1a2lem7  10171  axcclem  10222  ttukeylem1  10274  fpwwe2lem5  10400  fpwwe2lem8  10403  canthp1lem2  10418  tskuni  10548  gruen  10577  cnexALT  12735  fiinfnf1o  14073  hasheqf1oi  14075  hashfacen  14175  hashfacenOLD  14176  fsumf1o  15444  fsumss  15446  fprodf1o  15665  fprodss  15667  ruc  15961  unbenlem  16618  xpsfrn  17288  xpsbas  17292  xpsadd  17294  xpsmul  17295  xpssca  17296  xpsvsca  17297  xpsless  17298  xpsle  17299  imasmndf1  18433  sursubmefmnd  18544  imasgrpf1  18701  gicsubgen  18903  symgmov2  19004  symgextfo  19039  symgfixelsi  19052  giccyg  19510  gsumzres  19519  gsumzcl2  19520  gsumzf1o  19522  gsumzaddlem  19531  gsumconst  19544  gsumzmhm  19547  gsumzoppg  19554  dprdf1o  19644  gsumfsum  20674  znleval  20771  lmimlbs  21052  lbslcic  21057  coe1mul2lem2  21448  cmpfi  22568  idqtop  22866  basqtop  22871  tgqtop  22872  hmeontr  22929  hmeoimaf1o  22930  hmeoqtop  22935  cmphmph  22948  connhmph  22949  nrmhmph  22954  indishmph  22958  cmphaushmeo  22960  xpstps  22970  xpstopnlem2  22971  fmid  23120  tsmsf1o  23305  imasdsf1olem  23535  imasf1oxmet  23537  imasf1omet  23538  xpsdsfn  23539  imasf1oxms  23654  imasf1oms  23655  iccpnfhmeo  24117  cnheiborlem  24126  ovolctb  24663  ovolicc2lem4  24693  dyadmbl  24773  mbfimaopnlem  24828  itg1addlem4  24872  itg1addlem4OLD  24873  dvcnvrelem2  25191  dvcnvre  25192  deg1ldg  25266  deg1leb  25269  efifo  25712  logrn  25723  dvrelog  25801  efopnlem2  25821  fsumdvdsmul  26353  f1otrg  27241  axcontlem10  27350  edgusgrnbfin  27749  eupthvdres  28608  cnvunop  30289  counop  30292  idunop  30349  elunop2  30384  fmptco1f1o  30977  padct  31063  symgcom  31361  cycpmconjvlem  31417  cycpmconjslem2  31431  xrge0iifiso  31894  volmeas  32208  ballotlemro  32498  derangenlem  33142  subfacp1lem3  33153  subfacp1lem5  33155  erdsze2lem1  33174  cvmsss2  33245  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem9  35795  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem14  35800  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem22  35808  poimirlem23  35809  poimirlem24  35810  poimirlem25  35811  poimirlem29  35815  poimirlem31  35817  mblfinlem2  35824  ismtybndlem  35973  ismtyres  35975  diaintclN  39079  dibintclN  39188  mapdrn  39670  dnnumch2  40877  kelac1  40895  lnmlmic  40920  pwslnmlem1  40924  pwfi2f1o  40928  gicabl  40931  imasgim  40932  isnumbasgrplem1  40933  ntrneifv2  41697  stoweidlem27  43575  fourierdlem20  43675  fourierdlem51  43705  fourierdlem52  43706  fourierdlem63  43717  fourierdlem64  43718  fourierdlem65  43719  fourierdlem102  43756  fourierdlem114  43768  sge0f1o  43927  nnfoctbdjlem  44000  isomenndlem  44075  ovnsubaddlem1  44115  f1oresf1o2  44794  isomuspgrlem2d  45294