Theorem f1ofo 6837

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

Syntax hints:   → wi 4  ^◡ccnv 5674  Fun wfun 6534  –onto→wfo 6538  –1-1-onto→wf1o 6539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1089  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547

This theorem is referenced by:  f1imacnv  6846  resin  6852  f1ococnv2  6857  fo00  6866  isoini  7331  isofrlem  7333  isoselem  7334  ncanth  7359  f1opw2  7657  f1dmex  7939  f1ovv  7940  f1oweALT  7955  wemoiso2  7957  curry1  8086  curry2  8089  smoiso2  8365  f1osetex  8849  bren  8945  brenOLD  8946  f1oeng  8963  en1  9017  en1OLD  9018  canth2  9126  domss2  9132  mapen  9137  ssenen  9147  dif1enlem  9152  dif1enlemOLD  9153  ssfiALT  9170  phplem2  9204  php3  9208  phplem4OLD  9216  php3OLD  9220  domunfican  9316  fiint  9320  f1fi  9335  f1opwfi  9352  mapfien  9399  supisolem  9464  ordiso2  9506  ordtypelem10  9518  oismo  9531  wdomref  9563  brwdom2  9564  unxpwdom2  9579  cantnflt2  9664  cantnfp1lem3  9671  wemapwe  9688  infxpenc2lem1  10010  fseqen  10018  infpwfien  10053  infmap2  10209  ackbij2  10234  cff1  10249  cofsmo  10260  infpssr  10299  enfin2i  10312  fin23lem27  10319  enfin1ai  10375  fin1a2lem7  10397  axcclem  10448  ttukeylem1  10500  fpwwe2lem5  10626  fpwwe2lem8  10629  canthp1lem2  10644  tskuni  10774  gruen  10803  cnexALT  12966  fiinfnf1o  14306  hasheqf1oi  14307  hashfacen  14409  hashfacenOLD  14410  fsumf1o  15665  fsumss  15667  fprodf1o  15886  fprodss  15888  ruc  16182  unbenlem  16837  xpsfrn  17510  xpsbas  17514  xpsadd  17516  xpsmul  17517  xpssca  17518  xpsvsca  17519  xpsless  17520  xpsle  17521  imasmndf1  18660  sursubmefmnd  18773  imasgrpf1  18936  gicsubgen  19146  symgmov2  19249  symgextfo  19284  symgfixelsi  19297  giccyg  19762  gsumzres  19771  gsumzcl2  19772  gsumzf1o  19774  gsumzaddlem  19783  gsumconst  19796  gsumzmhm  19799  gsumzoppg  19806  dprdf1o  19896  imasringf1  20137  gsumfsum  21004  znleval  21101  lmimlbs  21382  lbslcic  21387  coe1mul2lem2  21781  cmpfi  22903  idqtop  23201  basqtop  23206  tgqtop  23207  hmeontr  23264  hmeoimaf1o  23265  hmeoqtop  23270  cmphmph  23283  connhmph  23284  nrmhmph  23289  indishmph  23293  cmphaushmeo  23295  xpstps  23305  xpstopnlem2  23306  fmid  23455  tsmsf1o  23640  imasdsf1olem  23870  imasf1oxmet  23872  imasf1omet  23873  xpsdsfn  23874  imasf1oxms  23989  imasf1oms  23990  iccpnfhmeo  24452  cnheiborlem  24461  ovolctb  24998  ovolicc2lem4  25028  dyadmbl  25108  mbfimaopnlem  25163  itg1addlem4  25207  itg1addlem4OLD  25208  dvcnvrelem2  25526  dvcnvre  25527  deg1ldg  25601  deg1leb  25604  efifo  26047  logrn  26058  dvrelog  26136  efopnlem2  26156  fsumdvdsmul  26688  f1otrg  28111  axcontlem10  28220  edgusgrnbfin  28619  eupthvdres  29477  cnvunop  31158  counop  31161  idunop  31218  elunop2  31253  fmptco1f1o  31844  padct  31931  symgcom  32231  cycpmconjvlem  32287  cycpmconjslem2  32301  xrge0iifiso  32903  volmeas  33217  ballotlemro  33509  derangenlem  34150  subfacp1lem3  34161  subfacp1lem5  34163  erdsze2lem1  34182  cvmsss2  34253  poimirlem1  36477  poimirlem2  36478  poimirlem3  36479  poimirlem4  36480  poimirlem5  36481  poimirlem6  36482  poimirlem7  36483  poimirlem9  36485  poimirlem10  36486  poimirlem11  36487  poimirlem12  36488  poimirlem14  36490  poimirlem15  36491  poimirlem16  36492  poimirlem17  36493  poimirlem19  36495  poimirlem20  36496  poimirlem22  36498  poimirlem23  36499  poimirlem24  36500  poimirlem25  36501  poimirlem29  36505  poimirlem31  36507  mblfinlem2  36514  ismtybndlem  36662  ismtyres  36664  diaintclN  39917  dibintclN  40026  mapdrn  40508  riccrng1  41093  ricdrng1  41099  dnnumch2  41772  kelac1  41790  lnmlmic  41815  pwslnmlem1  41819  pwfi2f1o  41823  gicabl  41826  imasgim  41827  isnumbasgrplem1  41828  ntrneifv2  42816  stoweidlem27  44729  fourierdlem20  44829  fourierdlem51  44859  fourierdlem52  44860  fourierdlem63  44871  fourierdlem64  44872  fourierdlem65  44873  fourierdlem102  44910  fourierdlem114  44922  sge0f1o  45084  nnfoctbdjlem  45157  isomenndlem  45232  ovnsubaddlem1  45272  f1oresf1o2  45985  isomuspgrlem2d  46485  imasrngf1  46665