Theorem f1of1 6774

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

Assertion

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

Proof of Theorem f1of1

Step	Hyp	Ref	Expression
1		df-f1o 6500	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
2	1	simplbi 496	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)

Syntax hints:   → wi 4  –1-1→wf1 6490  –onto→wfo 6491  –1-1-onto→wf1o 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-f1o 6500

This theorem is referenced by:  f1of  6775  f1un  6795  f1sng  6818  f1oresrab  7075  f1ounsn  7221  f1prex  7233  f1ocnvfvrneq  7235  f1ocoima  7252  isof1oidb  7273  isores3  7284  isoini2  7288  isosolem  7296  f1oiso  7300  weniso  7303  weisoeq  7304  f1opw2  7616  f1ovv  7905  mptcnfimad  7933  tposf12  8195  oacomf1olem  8493  enssdom  8917  enssdomOLD  8918  domssex2  9069  mapen  9073  ssenen  9083  ssfiALT  9102  ssdomfi  9124  ssdomfi2  9125  sucdom2  9131  phplem2  9133  php3  9137  snnen2o  9149  1sdom2dom  9158  f1finf1o  9177  domunfican  9226  fiint  9231  f1opwfi  9260  mapfienlem1  9312  mapfienlem2  9313  mapfien  9315  marypha1lem  9340  ordtypelem10  9436  oiexg  9444  unxpwdom2  9497  wemapwe  9612  inlresf1  9833  inrresf1  9835  isinffi  9910  infxpenlem  9929  fseqenlem1  9940  dfac12lem2  10061  dfac12r  10063  ackbij2  10158  cff1  10174  infpssrlem4  10222  fin4en1  10225  enfin2i  10237  fin23lem28  10256  isf32lem7  10275  isf34lem3  10291  enfin1ai  10300  canthnum  10566  canthwe  10568  canthp1lem2  10570  pwfseqlem4  10579  pwfseqlem5  10580  tskuni  10700  grothomex  10746  negfi  12099  seqf1olem1  13997  hashfacen  14410  hashf1lem1  14411  fsumss  15681  ackbijnn  15787  fprodss  15907  bitsinv2  16406  bitsf1  16409  sadasslem  16433  sadeq  16435  phimullem  16743  eulerthlem2  16746  unbenlem  16873  f1ocpbllem  17482  f1ovscpbl  17484  xpsff1o2  17527  xpsmnd  18739  injsubmefmnd  18859  xpsgrp  19029  eqgen  19150  conjsubgen  19220  subggim  19235  gim0to0  19238  gicsubgen  19248  symgfvne  19350  symgextf1  19390  symgfixelsi  19404  f1omvdmvd  19412  f1omvdconj  19415  pmtrfconj  19435  odngen  19546  sylow1lem2  19568  sylow2blem1  19589  gsumzres  19878  gsumzcl2  19879  gsumzf1o  19881  gsumzaddlem  19890  gsumconst  19903  gsumzmhm  19906  gsumzoppg  19913  dprdf1o  20003  xpsrngd  20154  xpsringd  20306  gsumfsum  21427  zntoslem  21549  znunithash  21557  iporthcom  21628  lindfres  21816  islindf3  21819  lindsmm  21821  lmimlbs  21829  lbslcic  21834  coe1sfi  22190  coe1mul2lem2  22246  resthauslem  23341  sshauslem  23350  basqtop  23689  tgqtop  23690  hmeoopn  23744  hmeocld  23745  hmeontr  23747  hmeoimaf1o  23748  haushmphlem  23765  tsmsf1o  24123  imasdsf1olem  24351  imasf1oxmet  24353  imasf1oxms  24467  ovoliunlem1  25482  dyadmbl  25580  vitalilem3  25590  dvcnvlem  25956  dvne0f1  25992  dvcnvrelem2  25998  logf1o2  26630  dvlog  26631  wilthlem3  27050  oldfib  28386  istrkg2ld  28545  f1otrg  28956  axcontlem10  29059  usgrf1  29258  usgrexmplef  29345  usgrres1  29401  edgusgrnbfin  29459  usgrexilem  29526  sizusglecusglem1  29548  uspgr2wlkeq  29732  trlres  29785  usgr2trlncl  29846  clwlkclwwlk  30090  adjbd1o  32174  padct  32809  indf1ofs  32944  s1f1  33021  s2f1  33023  mndlactf1o  33108  mndractf1o  33109  gsumwrd2dccat  33157  cycpmconjv  33221  1arithidomlem2  33614  mplvrpmlem  33705  mplvrpmfgalem  33706  mplvrpmga  33707  mplvrpmmhm  33708  mplvrpmrhm  33709  esplysply  33733  lmimdim  33766  madjusmdetlem4  33993  tpr2rico  34075  qqhre  34183  eulerpartgbij  34535  eulerpartlemgh  34541  ballotlemscr  34682  ballotlemro  34686  ballotlemfrc  34690  ballotlemrinv0  34696  reprpmtf1o  34789  onvf1od  35308  vonf1owev  35309  derangenlem  35372  subfacp1lem3  35383  subfacp1lem5  35385  erdsze2lem1  35404  cvmliftmolem1  35482  cvmlift2lem9a  35504  phpreu  37942  poimirlem1  37959  poimirlem4  37962  poimirlem9  37967  poimirlem22  37980  mblfinlem2  37996  metf1o  38093  ismtyima  38141  ismtyres  38146  rngoisocnv  38319  laut11  40549  diaf1oN  41593  mapdcnvcl  42115  mapdcnvid2  42120  ricdrng1  42990  evlselv  43037  eldioph2lem2  43210  eldioph2  43211  pwfi2f1o  43545  gicabl  43548  permaxext  45453  permac8prim  45462  sge0f1o  46831  nnfoctbdjlem  46904  3f1oss1  47538  f1ocof1ob2  47545  f1oresf1o  47753  fundcmpsurbijinjpreimafv  47882  fundcmpsurinjpreimafv  47883  fundcmpsurinjimaid  47886  grimcnv  48379  uhgrimedg  48382  isuspgrim0lem  48384  isuspgrim0  48385  isuspgrimlem  48386  upgrimtrlslem2  48396  upgrimpthslem2  48399  uhgrimisgrgriclem  48421  uhgrimisgrgric  48422  clnbgrgrimlem  48424  grimedg  48426  grtriproplem  48430  grtrif1o  48433  grimgrtri  48440  stgrusgra  48450  isubgr3stgrlem4  48460  isubgr3stgrlem7  48463  isubgr3stgrlem8  48464  grlimgrtri  48494  usgrexmpl1lem  48512  usgrexmpl2lem  48517  gpgusgra  48548  imaidfu  49600  uptrlem1  49700