Theorem f1of1 6801

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

Syntax hints:   → wi 4  –1-1→wf1 6510  –onto→wfo 6511  –1-1-onto→wf1o 6512

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 6520

This theorem is referenced by:  f1of  6802  f1un  6822  f1sng  6844  f1oresrab  7101  f1ounsn  7249  f1prex  7261  f1ocnvfvrneq  7263  f1ocoima  7280  isof1oidb  7301  isores3  7312  isoini2  7316  isosolem  7324  f1oiso  7328  weniso  7331  weisoeq  7332  f1opw2  7646  f1ovv  7938  mptcnfimad  7967  tposf12  8232  oacomf1olem  8530  enssdom  8950  sucdom2OLD  9055  domssex2  9106  mapen  9110  ssenen  9120  ssfiALT  9143  ssdomfi  9165  ssdomfi2  9166  sucdom2  9172  phplem2  9174  php3  9178  snnen2o  9190  1sdom2dom  9200  f1finf1o  9222  f1finf1oOLD  9223  domunfican  9278  fiint  9283  fiintOLD  9284  f1opwfi  9313  mapfienlem1  9362  mapfienlem2  9363  mapfien  9365  marypha1lem  9390  ordtypelem10  9486  oiexg  9494  unxpwdom2  9547  wemapwe  9656  inlresf1  9874  inrresf1  9876  isinffi  9951  infxpenlem  9972  fseqenlem1  9983  dfac12lem2  10104  dfac12r  10106  ackbij2  10201  cff1  10217  infpssrlem4  10265  fin4en1  10268  enfin2i  10280  fin23lem28  10299  isf32lem7  10318  isf34lem3  10334  enfin1ai  10343  canthnum  10608  canthwe  10610  canthp1lem2  10612  pwfseqlem4  10621  pwfseqlem5  10622  tskuni  10742  grothomex  10788  negfi  12138  seqf1olem1  14012  hashfacen  14425  hashf1lem1  14426  fsumss  15697  ackbijnn  15800  fprodss  15920  bitsinv2  16419  bitsf1  16422  sadasslem  16446  sadeq  16448  phimullem  16755  eulerthlem2  16758  unbenlem  16885  f1ocpbllem  17493  f1ovscpbl  17495  xpsff1o2  17538  xpsmnd  18710  injsubmefmnd  18830  xpsgrp  18997  eqgen  19119  conjsubgen  19189  subggim  19204  gim0to0  19207  gicsubgen  19217  symgfvne  19317  symgextf1  19357  symgfixelsi  19371  f1omvdmvd  19379  f1omvdconj  19382  pmtrfconj  19402  odngen  19513  sylow1lem2  19535  sylow2blem1  19556  gsumzres  19845  gsumzcl2  19846  gsumzf1o  19848  gsumzaddlem  19857  gsumconst  19870  gsumzmhm  19873  gsumzoppg  19880  dprdf1o  19970  xpsrngd  20094  xpsringd  20247  gsumfsum  21357  zntoslem  21472  znunithash  21480  iporthcom  21550  lindfres  21738  islindf3  21741  lindsmm  21743  lmimlbs  21751  lbslcic  21756  coe1sfi  22104  coe1mul2lem2  22160  resthauslem  23256  sshauslem  23265  basqtop  23604  tgqtop  23605  hmeoopn  23659  hmeocld  23660  hmeontr  23662  hmeoimaf1o  23663  haushmphlem  23680  tsmsf1o  24038  imasdsf1olem  24267  imasf1oxmet  24269  imasf1oxms  24383  ovoliunlem1  25409  dyadmbl  25507  vitalilem3  25517  dvcnvlem  25886  dvne0f1  25923  dvcnvrelem2  25929  logf1o2  26565  dvlog  26566  wilthlem3  26986  istrkg2ld  28393  f1otrg  28804  axcontlem10  28906  usgrf1  29105  usgrexmplef  29192  usgrres1  29248  edgusgrnbfin  29306  usgrexilem  29373  sizusglecusglem1  29395  uspgr2wlkeq  29580  trlres  29634  usgr2trlncl  29696  clwlkclwwlk  29937  adjbd1o  32020  padct  32649  indf1ofs  32795  s1f1  32870  s2f1  32872  mndlactf1o  32977  mndractf1o  32978  gsumwrd2dccat  33013  cycpmconjv  33105  1arithidomlem2  33513  lmimdim  33605  madjusmdetlem4  33826  tpr2rico  33908  qqhre  34016  eulerpartgbij  34369  eulerpartlemgh  34375  ballotlemscr  34516  ballotlemro  34520  ballotlemfrc  34524  ballotlemrinv0  34530  reprpmtf1o  34623  derangenlem  35158  subfacp1lem3  35169  subfacp1lem5  35171  erdsze2lem1  35190  cvmliftmolem1  35268  cvmlift2lem9a  35290  phpreu  37593  poimirlem1  37610  poimirlem4  37613  poimirlem9  37618  poimirlem22  37631  mblfinlem2  37647  metf1o  37744  ismtyima  37792  ismtyres  37797  rngoisocnv  37970  laut11  40075  diaf1oN  41119  mapdcnvcl  41641  mapdcnvid2  41646  ricdrng1  42509  evlselv  42568  eldioph2lem2  42742  eldioph2  42743  pwfi2f1o  43078  gicabl  43081  permaxext  44988  permac8prim  44997  sge0f1o  46373  nnfoctbdjlem  46446  3f1oss1  47066  f1ocof1ob2  47073  f1oresf1o  47281  fundcmpsurbijinjpreimafv  47398  fundcmpsurinjpreimafv  47399  fundcmpsurinjimaid  47402  grimcnv  47878  uhgrimedg  47881  isuspgrim0lem  47883  isuspgrim0  47884  isuspgrimlem  47885  upgrimtrlslem2  47895  upgrimpthslem2  47898  uhgrimisgrgriclem  47920  uhgrimisgrgric  47921  clnbgrgrimlem  47923  grimedg  47925  grtriproplem  47928  grtrif1o  47931  grimgrtri  47938  stgrusgra  47948  isubgr3stgrlem4  47958  isubgr3stgrlem7  47961  isubgr3stgrlem8  47962  grlimgrtri  47985  usgrexmpl1lem  48002  usgrexmpl2lem  48007  gpgusgra  48038  imaidfu  49087  uptrlem1  49183