Theorem f1of1 6823

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

This proof depends on syntax axioms:   → wi 4  –1-1→wf1 6537  –onto→wfo 6538  –1-1-onto→wf1o 6539

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 6547

This theorem is used by:  f1of  6824  f1un  6845  f1sng  6868  f1oresrab  7127  f1ounsn  7279  f1prex  7291  f1ocnvfvrneq  7293  f1ocoima  7310  isof1oidb  7331  isores3  7342  isoini2  7346  isosolem  7354  f1oiso  7358  weniso  7363  weisoeq  7364  f1opw2  7675  f1ovv  7961  mptcnfimad  7989  tposf12  8253  oacomf1olem  8555  enssdom  8979  enssdomOLD  8980  domssex2  9132  mapen  9136  ssenen  9146  ssfiALT  9165  ssdomfi  9187  ssdomfi2  9188  sucdom2  9194  phplem2  9196  php3  9200  snnen2o  9212  1sdom2dom  9221  f1finf1o  9240  domunfican  9288  fiint  9293  f1opwfi  9320  mapfienlem1  9372  mapfienlem2  9373  mapfien  9375  marypha1lem  9400  ordtypelem10  9496  oiexg  9504  unxpwdom2  9557  wemapwe  9673  inlresf1  9917  inrresf1  9919  isinffi  9994  infxpenlem  10013  fseqenlem1  10024  dfac12lem2  10144  dfac12r  10146  ackbij2  10241  cff1  10257  infpssrlem4  10305  fin4en1  10308  enfin2i  10320  fin23lem28  10339  isf32lem7  10358  isf34lem3  10374  enfin1ai  10383  canthnum  10649  canthwe  10651  canthp1lem2  10653  pwfseqlem4  10662  pwfseqlem5  10663  tskuni  10783  grothomex  10829  negfi  12179  seqf1olem1  14095  hashfacen  14509  hashf1lem1  14510  s1f1  14666  fsumss  15799  ackbijnn  15905  fprodss  16025  bitsinv2  16523  bitsf1  16526  sadasslem  16550  sadeq  16552  phimullem  16860  eulerthlem2  16863  unbenlem  16990  f1ocpbllem  17600  f1ovscpbl  17602  xpsff1o2  17645  xpsmnd  18872  injsubmefmnd  18993  xpsgrp  19169  eqgen  19293  conjsubgen  19365  subggim  19380  gim0to0  19383  gicsubgen  19393  symgfvne  19495  symgextf1  19535  symgfixelsi  19549  f1omvdmvd  19557  f1omvdconj  19560  pmtrfconj  19580  odngen  19691  sylow1lem2  19713  sylow2blem1  19734  gsumzres  20023  gsumzcl2  20024  gsumzf1o  20026  gsumzaddlem  20035  gsumconst  20048  gsumzmhm  20051  gsumzoppg  20058  dprdf1o  20148  xpsrngd  20301  xpsringd  20460  gsumfsum  21634  zntoslem  21756  znunithash  21764  iporthcom  21835  lindfres  22023  islindf3  22026  lindsmm  22028  lmimlbs  22036  lbslcic  22041  coe1sfi  22423  coe1mul2lem2  22479  resthauslem  23570  sshauslem  23579  basqtop  23919  tgqtop  23920  hmeoopn  23974  hmeocld  23975  hmeontr  23977  hmeoimaf1o  23978  haushmphlem  23995  tsmsf1o  24353  imasdsf1olem  24581  imasf1oxmet  24583  imasf1oxms  24697  ovoliunlem1  25712  dyadmbl  25810  vitalilem3  25820  dvcnvlem  26186  dvne0f1  26222  dvcnvrelem2  26228  logf1o2  26866  dvlog  26867  wilthlem3  27285  oldfib  28621  istrkg2ld  28780  f1otrg  29275  axcontlem10  29378  usgrf1  29580  usgrexmplef  29667  usgrres1  29723  edgusgrnbfin  29781  usgrexilem  29848  sizusglecusglem1  29869  uspgr2wlkeq  30053  trlres  30110  usgr2trlncl  30173  clwlkclwwlk  30420  adjbd1o  32508  padct  33133  indf1ofs  33256  s2f1  33333  mndlactf1o  33414  mndractf1o  33415  gsumwrd2dccat  33462  cycpmconjv  33526  1arithidomlem2  33890  mplvrpmlem  33997  mplvrpmfgalem  33998  mplvrpmga  33999  mplvrpmmhm  34000  mplvrpmrhm  34001  esplysply  34025  lmimdim  34058  madjusmdetlem4  34284  tpr2rico  34366  qqhre  34474  eulerpartgbij  34827  eulerpartlemgh  34833  ballotlemscr  34974  ballotlemro  34978  ballotlemfrc  34982  ballotlemrinv0  34988  reprpmtf1o  35078  onvf1od  35648  vonf1owev  35650  vonf1owevOLD  35651  vonf1oonf1  35655  derangenlem  35700  subfacp1lem3  35711  subfacp1lem5  35713  erdsze2lem1  35732  cvmliftmolem1  35810  cvmlift2lem9a  35832  phpreu  38312  poimirlem1  38329  poimirlem4  38332  poimirlem9  38337  poimirlem22  38350  mblfinlem2  38366  metf1o  38464  ismtyima  38512  ismtyres  38517  rngoisocnv  38690  laut11  40918  diaf1oN  41962  mapdcnvcl  42484  mapdcnvid2  42489  ricdrng1  43354  evlselv  43379  eldioph2lem2  43550  eldioph2  43551  pwfi2f1o  43881  gicabl  43884  permaxext  45772  permac8prim  45781  sge0f1o  47154  nnfoctbdjlem  47227  3f1oss1  47870  f1ocof1ob2  47877  f1oresf1o  48085  fundcmpsurbijinjpreimafv  48214  fundcmpsurinjpreimafv  48215  fundcmpsurinjimaid  48218  grimcnv  48711  uhgrimedg  48714  isuspgrim0lem  48716  isuspgrim0  48717  isuspgrimlem  48718  upgrimtrlslem2  48728  upgrimpthslem2  48731  uhgrimisgrgriclem  48753  uhgrimisgrgric  48754  clnbgrgrimlem  48756  grimedg  48758  grtriproplem  48762  grtrif1o  48765  grimgrtri  48772  stgrusgra  48782  isubgr3stgrlem4  48792  isubgr3stgrlem7  48795  isubgr3stgrlem8  48796  grlimgrtri  48826  usgrexmpl1lem  48844  usgrexmpl2lem  48849  gpgusgra  48880  imaidfu  49945  uptrlem1  50045