Theorem f1ofo 6789

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

Syntax hints:   → wi 4  ^◡ccnv 5630  Fun wfun 6493  –onto→wfo 6497  –1-1-onto→wf1o 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-cleq 2721  df-ss 3928  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506

This theorem is referenced by:  f1imacnv  6798  resin  6804  f1ococnv2  6809  fo00  6818  f1ounsn  7229  f1ocoima  7260  isoini  7295  isofrlem  7297  isoselem  7298  ncanth  7324  f1opw2  7624  f1dmex  7915  f1ovv  7916  f1oweALT  7930  wemoiso2  7932  mptcnfimad  7944  curry1  8060  curry2  8063  smoiso2  8315  f1osetex  8809  bren  8905  f1oeng  8919  en1  8972  canth2  9071  domss2  9077  mapen  9082  ssenen  9092  dif1enlem  9097  dif1enlemOLD  9098  ssfiALT  9115  phplem2  9146  php3  9150  f1fi  9239  domunfican  9248  fiint  9253  fiintOLD  9254  f1opwfi  9283  mapfien  9335  supisolem  9401  ordiso2  9444  ordtypelem10  9456  oismo  9469  wdomref  9501  brwdom2  9502  unxpwdom2  9517  cantnflt2  9602  cantnfp1lem3  9609  wemapwe  9626  infxpenc2lem1  9948  fseqen  9956  infpwfien  9991  infmap2  10146  ackbij2  10171  cff1  10187  cofsmo  10198  infpssr  10237  enfin2i  10250  fin23lem27  10257  enfin1ai  10313  fin1a2lem7  10335  axcclem  10386  ttukeylem1  10438  fpwwe2lem5  10564  fpwwe2lem8  10567  canthp1lem2  10582  tskuni  10712  gruen  10741  cnexALT  12921  fiinfnf1o  14291  hasheqf1oi  14292  hashfacen  14395  fsumf1o  15665  fsumss  15667  fprodf1o  15888  fprodss  15890  ruc  16187  unbenlem  16855  xpsfrn  17507  xpsbas  17511  xpsadd  17513  xpsmul  17514  xpssca  17515  xpsvsca  17516  xpsless  17517  xpsle  17518  imasmndf1  18685  sursubmefmnd  18805  imasgrpf1  18971  gicsubgen  19193  symgmov2  19302  symgextfo  19336  symgfixelsi  19349  giccyg  19814  gsumzres  19823  gsumzcl2  19824  gsumzf1o  19826  gsumzaddlem  19835  gsumconst  19848  gsumzmhm  19851  gsumzoppg  19858  dprdf1o  19948  imasrngf1  20098  imasringf1  20251  gsumfsum  21376  znleval  21496  lmimlbs  21778  lbslcic  21783  coe1mul2lem2  22187  cmpfi  23328  idqtop  23626  basqtop  23631  tgqtop  23632  hmeontr  23689  hmeoimaf1o  23690  hmeoqtop  23695  cmphmph  23708  connhmph  23709  nrmhmph  23714  indishmph  23718  cmphaushmeo  23720  xpstps  23730  xpstopnlem2  23731  fmid  23880  tsmsf1o  24065  imasdsf1olem  24294  imasf1oxmet  24296  imasf1omet  24297  xpsdsfn  24298  imasf1oxms  24410  imasf1oms  24411  iccpnfhmeo  24876  cnheiborlem  24886  ovolctb  25424  ovolicc2lem4  25454  dyadmbl  25534  mbfimaopnlem  25589  itg1addlem4  25633  dvcnvrelem2  25956  dvcnvre  25957  deg1ldg  26030  deg1leb  26033  efifo  26489  logrn  26500  dvrelog  26579  efopnlem2  26599  fsumdvdsmul  27138  fsumdvdsmulOLD  27140  f1otrg  28851  axcontlem10  28953  edgusgrnbfin  29353  eupthvdres  30214  cnvunop  31897  counop  31900  idunop  31957  elunop2  31992  fmptco1f1o  32607  padct  32693  mndlactf1o  33014  mndractf1o  33015  symgcom  33055  cycpmconjvlem  33113  cycpmconjslem2  33127  1arithidomlem2  33500  xrge0iifiso  33918  volmeas  34214  ballotlemro  34507  derangenlem  35151  subfacp1lem3  35162  subfacp1lem5  35164  erdsze2lem1  35183  cvmsss2  35254  poimirlem1  37608  poimirlem2  37609  poimirlem3  37610  poimirlem4  37611  poimirlem5  37612  poimirlem6  37613  poimirlem7  37614  poimirlem9  37616  poimirlem10  37617  poimirlem11  37618  poimirlem12  37619  poimirlem14  37621  poimirlem15  37622  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem22  37629  poimirlem23  37630  poimirlem24  37631  poimirlem25  37632  poimirlem29  37636  poimirlem31  37638  mblfinlem2  37645  ismtybndlem  37793  ismtyres  37795  diaintclN  41045  dibintclN  41154  mapdrn  41636  aks6d1c1p5  42093  riccrng1  42502  ricdrng1  42509  dnnumch2  43027  kelac1  43045  lnmlmic  43070  pwslnmlem1  43074  pwfi2f1o  43078  gicabl  43081  imasgim  43082  isnumbasgrplem1  43083  ntrneifv2  44062  stoweidlem27  46018  fourierdlem20  46118  fourierdlem51  46148  fourierdlem52  46149  fourierdlem63  46160  fourierdlem64  46161  fourierdlem65  46162  fourierdlem102  46199  fourierdlem114  46211  sge0f1o  46373  nnfoctbdjlem  46446  isomenndlem  46521  ovnsubaddlem1  46561  3f1oss1  47069  f1oresf1o2  47285  grimuhgr  47880  grimcnv  47881  isuspgrimlem  47888  grimedg  47928  isubgr3stgrlem8  47965  tposres3  48862  uptrlem1  49192  lmdran  49653  cmdlan  49654