Theorem f1of1 6853

Description: A one-to-one onto mapping is a one-to-one mapping. (Contributed by NM, 12-Dec-2003.)

Assertion

Ref	Expression
f1of1	⊢ (𝐹:𝐴⟶1-1onto𝐵 → 𝐹:𝐴⟶1-1𝐵)

Proof of Theorem f1of1

Step	Hyp	Ref	Expression
1		df-f1o 6573	. 2 ⊢ (𝐹:𝐴⟶1-1onto𝐵 ↔ (𝐹:𝐴⟶1-1𝐵 ∧ 𝐹:𝐴⟶onto𝐵))
2	1	simplbi 502	1 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → 𝐹:𝐴⟶1-1𝐵)

This proof depends on syntax axioms:   → wi 4  ⟶1-1wf1 6563  ⟶ontowfo 6564  ⟶1-1ontowf1o 6565

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f1o 6573

This theorem is used by:  f1of  6854  f1un  6875  f1sng  6899  f1oresrab  7160  f1ounsn  7311  f1prex  7323  f1ocnvfvrneq  7325  f1ocoima  7342  isof1oidb  7363  isores3  7374  isoini2  7378  isosolem  7386  f1oiso  7390  weniso  7395  weisoeq  7396  f1opw2  7708  f1ovv  8004  mptcnfimad  8032  tposf12  8306  oacomf1olem  8610  enssdom  9041  enssdomOLD  9042  domssex2  9194  mapen  9198  ssenen  9208  ssfiALT  9227  ssdomfi  9249  ssdomfi2  9250  sucdom2  9256  phplem2  9258  php3  9262  snnen2o  9274  1sdom2dom  9283  f1finf1o  9302  domunfican  9351  fiint  9356  f1opwfi  9383  mapfienlem1  9434  mapfienlem2  9435  mapfien  9437  marypha1lem  9462  ordtypelem10  9558  oiexg  9566  unxpwdom2  9619  wemapwe  9735  inlresf1  10033  inrresf1  10035  isinffi  10112  infxpenlem  10131  fseqenlem1  10142  dfac12lem2  10262  dfac12r  10264  ackbij2  10359  cff1  10375  infpssrlem4  10423  fin4en1  10426  enfin2i  10438  fin23lem28  10457  isf32lem7  10476  isf34lem3  10492  enfin1ai  10501  canthnum  10773  canthwe  10775  canthp1lem2  10777  pwfseqlem4  10786  pwfseqlem5  10787  tskuni  10907  grothomex  10953  negfi  12306  seqf1olem1  14224  hashfacen  14640  hashf1lem1  14641  s1f1  14798  fsumss  15935  ackbijnn  16041  fprodss  16159  bitsinv2  16657  bitsf1  16660  sadasslem  16684  sadeq  16686  phimullem  17000  eulerthlem2  17003  unbenlem  17130  f1ocpbllem  17746  f1ovscpbl  17748  xpsff1o2  17791  xpsmnd  19021  injsubmefmnd  19143  xpsgrp  19319  eqgen  19443  conjsubgen  19515  subggim  19530  gim0to0  19533  gicsubgen  19544  symgfvne  19646  symgextf1  19686  symgfixelsi  19700  f1omvdmvd  19708  f1omvdconj  19711  pmtrfconj  19731  odngen  19842  sylow1lem2  19864  sylow2blem1  19885  gsumzres  20174  gsumzcl2  20175  gsumzf1o  20177  gsumzaddlem  20186  gsumconst  20199  gsumzmhm  20202  gsumzoppg  20209  dprdf1o  20299  xpsrngd  20452  xpsringd  20613  gsumfsum  21794  zntoslem  21917  znunithash  21925  iporthcom  21996  lindfres  22184  islindf3  22187  lindsmm  22189  lmimlbs  22197  lbslcic  22202  coe1sfi  22586  coe1mul2lem2  22642  resthauslem  23736  sshauslem  23745  basqtop  24085  tgqtop  24086  hmeoopn  24140  hmeocld  24141  hmeontr  24143  hmeoimaf1o  24144  haushmphlem  24161  tsmsf1o  24519  imasdsf1olem  24747  imasf1oxmet  24749  imasf1oxms  24863  ovoliunlem1  25878  dyadmbl  25976  vitalilem3  25986  dvcnvlem  26351  dvne0f1  26387  dvcnvrelem2  26393  logf1o2  27035  dvlog  27036  wilthlem3  27454  oldfib  28820  istrkg2ld  28979  f1otrg  29505  axcontlem10  29608  usgrf1  29810  usgrexmplef  29897  usgrres1  29953  edgusgrnbfin  30011  usgrexilem  30078  sizusglecusglem1  30099  uspgr2wlkeq  30283  trlres  30340  usgr2trlncl  30403  clwlkclwwlk  30650  adjbd1o  32744  padct  33407  indf1ofs  33529  s2f1  33606  mndlactf1o  33690  mndractf1o  33691  gsumwrd2dccat  33738  cycpmconjv  33802  1arithidomlem2  34172  mplvrpmlem  34286  mplvrpmfgalem  34287  mplvrpmga  34288  mplvrpmmhm  34289  mplvrpmrhm  34290  esplysply  34314  lmimdim  34347  madjusmdetlem4  34573  tpr2rico  34655  qqhre  34763  eulerpartgbij  35115  eulerpartlemgh  35121  ballotlemscr  35262  ballotlemro  35266  ballotlemfrc  35270  ballotlemrinv0  35276  reprpmtf1o  35366  dfac15  35886  jf1  36051  onvf1od  36076  vonf1owev  36078  vonf1owevOLD  36079  vonf1oonf1  36084  vonf1onprcf1ac  36085  onprcf1acwevd  36088  onprcf1of1orad  36094  onprcf1of1orbd  36095  derangenlem  36144  subfacp1lem3  36155  subfacp1lem5  36157  erdsze2lem1  36176  cvmliftmolem1  36254  cvmlift2lem9a  36276  phpreu  38795  poimirlem1  38807  poimirlem4  38810  poimirlem9  38815  poimirlem22  38828  mblfinlem2  38844  metf1o  38955  ismtyima  39003  ismtyres  39008  rngoisocnv  39181  laut11  41409  diaf1oN  42453  mapdcnvcl  42975  mapdcnvid2  42980  ricdrng1  43858  evlselv  43883  eldioph2lem2  44038  eldioph2  44039  pwfi2f1o  44364  gicabl  44367  permaxext  46259  permac8prim  46268  hfstructwe  46303  sge0f1o  47665  nnfoctbdjlem  47738  3f1oss1  48418  f1ocof1ob2  48425  f1oresf1o  48633  fundcmpsurbijinjpreimafv  48762  fundcmpsurinjpreimafv  48763  fundcmpsurinjimaid  48766  grimcnv  49259  uhgrimedg  49262  isuspgrim0lem  49264  isuspgrim0  49265  isuspgrimlem  49266  upgrimtrlslem2  49276  upgrimpthslem2  49279  uhgrimisgrgriclem  49301  uhgrimisgrgric  49302  clnbgrgrimlem  49304  grimedg  49306  grtriproplem  49310  grtrif1o  49313  grimgrtri  49320  stgrusgra  49330  isubgr3stgrlem4  49340  isubgr3stgrlem7  49343  isubgr3stgrlem8  49344  grlimgrtri  49374  usgrexmpl1lem  49392  usgrexmpl2lem  49397  gpgusgra  49428  imaidfu  50557  uptrlem1  50657