Theorem f1ofo 6829

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

Syntax hints:   → wi 4  ^◡ccnv 5661  Fun wfun 6531  –onto→wfo 6535  –1-1-onto→wf1o 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-ex 1807  df-cleq 2761  df-ss 3930  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544

This theorem is referenced by:  f1imacnv  6838  resin  6844  f1ococnv2  6849  fo00  6858  f1ounsn  7271  f1ocoima  7302  isoini  7337  isofrlem  7339  isoselem  7340  ncanth  7366  f1opw2  7666  f1dmex  7954  f1ovv  7955  f1oweALT  7969  wemoiso2  7971  mptcnfimad  7983  curry1  8099  curry2  8102  smoiso2  8356  f1osetex  8856  bren  8953  f1oeng  8967  en1  9021  canth2  9118  domss2  9124  mapen  9129  ssenen  9139  dif1enlem  9144  ssfiALT  9158  phplem2  9189  php3  9193  f1fi  9274  domunfican  9281  fiint  9286  f1opwfi  9313  mapfien  9368  supisolem  9434  ordiso2  9477  ordtypelem10  9489  oismo  9502  wdomref  9534  brwdom2  9535  unxpwdom2  9550  cantnflt2  9642  cantnfp1lem3  9649  wemapwe  9666  infxpenc2lem1  10003  fseqen  10011  infpwfien  10046  infmap2  10200  ackbij2  10225  cff1  10242  cofsmo  10253  infpssr  10292  enfin2i  10305  fin23lem27  10312  enfin1ai  10368  fin1a2lem7  10390  axcclem  10441  ttukeylem1  10493  fpwwe2lem5  10620  fpwwe2lem8  10623  canthp1lem2  10638  tskuni  10768  gruen  10797  cnexALT  13010  fiinfnf1o  14386  hasheqf1oi  14387  hashfacen  14491  fsumf1o  15774  fsumss  15776  fprodf1o  16000  fprodss  16002  ruc  16299  unbenlem  16968  xpsfrn  17622  xpsbas  17626  xpsadd  17628  xpsmul  17629  xpssca  17630  xpsvsca  17631  xpsless  17632  xpsle  17633  imasmndf1  18834  sursubmefmnd  18955  imasgrpf1  19123  gicsubgen  19349  symgmov2  19458  symgextfo  19492  symgfixelsi  19505  giccyg  19970  gsumzres  19979  gsumzcl2  19980  gsumzf1o  19982  gsumzaddlem  19991  gsumconst  20004  gsumzmhm  20007  gsumzoppg  20014  dprdf1o  20104  imasrngf1  20256  imasringf1  20413  gsumfsum  21553  znleval  21673  lmimlbs  21955  lbslcic  21960  coe1mul2lem2  22398  cmpfi  23534  idqtop  23832  basqtop  23837  tgqtop  23838  hmeontr  23895  hmeoimaf1o  23896  hmeoqtop  23901  cmphmph  23914  connhmph  23915  nrmhmph  23920  indishmph  23924  cmphaushmeo  23926  xpstps  23936  xpstopnlem2  23937  fmid  24086  tsmsf1o  24271  imasdsf1olem  24499  imasf1oxmet  24501  imasf1omet  24502  xpsdsfn  24503  imasf1oxms  24615  imasf1oms  24616  iccpnfhmeo  25073  cnheiborlem  25082  ovolctb  25618  ovolicc2lem4  25648  dyadmbl  25728  mbfimaopnlem  25783  itg1addlem4  25827  dvcnvrelem2  26146  dvcnvre  26147  deg1ldg  26218  deg1leb  26221  efifo  26678  logrn  26689  dvrelog  26768  efopnlem2  26788  fsumdvdsmul  27325  f1otrg  29161  axcontlem10  29264  edgusgrnbfin  29664  eupthvdres  30527  cnvunop  32211  counop  32214  idunop  32271  elunop2  32306  fmptco1f1o  32919  padct  33004  mndlactf1o  33291  mndractf1o  33292  symgcom  33344  cycpmconjvlem  33402  cycpmconjslem2  33416  1arithidomlem2  33771  esplysply  33906  xrge0iifiso  34270  volmeas  34566  ballotlemro  34858  vonf1oonfo  35498  derangenlem  35562  subfacp1lem3  35573  subfacp1lem5  35575  erdsze2lem1  35594  cvmsss2  35665  poimirlem1  38160  poimirlem2  38161  poimirlem3  38162  poimirlem4  38163  poimirlem5  38164  poimirlem6  38165  poimirlem7  38166  poimirlem9  38168  poimirlem10  38169  poimirlem11  38170  poimirlem12  38171  poimirlem14  38173  poimirlem15  38174  poimirlem16  38175  poimirlem17  38176  poimirlem19  38178  poimirlem20  38179  poimirlem22  38181  poimirlem23  38182  poimirlem24  38183  poimirlem25  38184  poimirlem29  38188  poimirlem31  38190  mblfinlem2  38197  ismtybndlem  38345  ismtyres  38347  diaintclN  41722  dibintclN  41831  mapdrn  42313  aks6d1c1p5  42769  riccrng1  43181  ricdrng1  43188  dnnumch2  43664  kelac1  43682  lnmlmic  43707  pwslnmlem1  43711  pwfi2f1o  43715  gicabl  43718  imasgim  43719  isnumbasgrplem1  43720  ntrneifv2  44698  stoweidlem27  46633  fourierdlem20  46733  fourierdlem51  46763  fourierdlem52  46764  fourierdlem63  46775  fourierdlem64  46776  fourierdlem65  46777  fourierdlem102  46814  fourierdlem114  46826  sge0f1o  46988  nnfoctbdjlem  47061  isomenndlem  47136  ovnsubaddlem1  47176  3f1oss1  47701  f1oresf1o2  47917  grimuhgr  48541  grimcnv  48542  isuspgrimlem  48549  grimedg  48589  isubgr3stgrlem8  48627  tposres3  49544  uptrlem1  49873  lmdran  50334  cmdlan  50335