Theorem sneq 3882

Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
sneq	|- ( A = B -> { A } = { B } )

Proof of Theorem sneq

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq2 2447	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2552	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3873	. 2 |- { A } = { x | x = A }
4		df-sn 3873	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2495	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1369   {cab 2424   {csn 3872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-sn 3873

This theorem is referenced by:  sneqi  3883  sneqd  3884  euabsn  3942  absneu  3944  preq1  3949  tpeq3  3960  snssg  4002  sneqrg  4037  sneqbg  4038  opeq1  4054  unisng  4102  opthwiener  4588  suceq  4779  opeliunxp  4885  relop  4985  elimasng  5190  xpdifid  5261  dmsnsnsn  5312  iotajust  5375  fconstg  5592  f1osng  5674  opabiotafun  5747  fsng  5877  fnressn  5889  fressnfv  5891  funfvima3  5949  isofrlem  6026  isoselem  6027  snnex  6377  elxp4  6517  elxp5  6518  1stval  6574  2ndval  6575  2ndval2  6590  fo1st  6591  fo2nd  6592  f1stres  6593  f2ndres  6594  mpt2mptsx  6632  dmmpt2ssx  6634  fmpt2x  6635  ovmptss  6649  fparlem3  6669  fparlem4  6670  suppval  6687  suppsnop  6699  ressuppssdif  6705  brtpos2  6746  dftpos4  6759  tpostpos  6760  eceq1  7129  fvdiagfn  7249  mapsncnv  7251  elixpsn  7294  ixpsnf1o  7295  ensn1g  7366  en1  7368  difsnen  7385  xpsneng  7388  xpcomco  7393  xpassen  7397  xpdom2  7398  canth2  7456  phplem3  7484  xpfi  7575  marypha2lem2  7678  cardsn  8131  pm54.43  8162  dfac5lem3  8287  dfac5lem4  8288  kmlem9  8319  kmlem11  8321  kmlem12  8322  ackbij1lem8  8388  r1om  8405  fictb  8406  hsmexlem4  8590  axcc2lem  8597  axcc2  8598  axdc3lem4  8614  fpwwe2cbv  8789  fpwwe2lem3  8792  fpwwecbv  8803  canth4  8806  fsum2dlem  13229  fsumcnv  13232  fsumcom2  13233  ackbijnn  13283  xpnnenOLD  13484  vdwlem1  14034  vdwlem12  14045  vdwlem13  14046  vdwnn  14051  0ram  14073  ramz2  14077  pwsval  14416  xpsfval  14497  xpsval  14502  symg2bas  15894  symgfixelsi  15931  pmtrfv  15949  pmtrprfval  15984  sylow2a  16109  efgrelexlema  16237  gsum2dlem2  16452  gsum2dOLD  16454  gsum2d2  16456  gsumcom2  16457  dprdcntz  16482  dprddisj  16483  dprd2dlem2  16529  dprd2dlem1  16530  dprd2da  16531  ablfac1eu  16564  ablfaclem3  16578  lssats2  17061  lspsneq0  17073  lbsind  17141  lspsneq  17183  lspdisj2  17188  lspsnsubn0  17201  lspprat  17214  islbs2  17215  lbsextlem4  17222  lbsextg  17223  lpi0  17309  lpi1  17310  psrvsca  17442  evlssca  17588  mpfind  17602  coe1fv  17642  coe1tm  17706  pf1ind  17769  frlmlbs  18205  lindfind  18225  lindsind  18226  lindfrn  18230  submaval  18372  mdetunilem3  18400  mdetunilem4  18401  mdetunilem9  18406  islp  18724  perfi  18739  t1sncld  18910  bwth  18993  dis2ndc  19044  nllyi  19059  ptbasfi  19134  txkgen  19205  xkofvcn  19237  xkoinjcn  19240  qtopeu  19269  txswaphmeolem  19357  pt1hmeo  19359  elflim2  19517  cnextfvval  19617  cnextcn  19619  cnextfres  19620  tsmsxplem1  19707  tsmsxplem2  19708  ucncn  19840  itg11  21149  i1faddlem  21151  i1fmullem  21152  itg1addlem3  21156  itg1mulc  21162  eldv  21353  ply1lpir  21630  areambl  22332  tglngval  22965  nb3graprlem2  23328  cusgrarn  23335  cusgra1v  23337  cusgra2v  23338  cusgra3v  23340  cusgrares  23348  usgrasscusgra  23359  sizeusglecusglem1  23360  uvtxel  23365  cusgrauvtxb  23372  vdgrval  23534  gxval  23713  h1de2ctlem  24926  spansn  24930  elspansn  24937  elspansn2  24938  spansneleq  24941  h1datom  24953  spansnj  25018  spansncv  25024  superpos  25726  sumdmdlem2  25791  dfcnv2  25962  sibfima  26693  sibfof  26695  cvmscbv  27116  cvmsdisj  27128  cvmsss2  27132  cvmliftlem15  27156  cvmlift2lem11  27171  cvmlift2lem12  27172  cvmlift2lem13  27173  fprod2dlem  27460  fprodcnv  27463  fprodcom2  27464  eldm3  27541  elima4  27559  predeq123  27595  fvsingle  27920  snelsingles  27922  dfiota3  27923  brapply  27938  funpartlem  27942  altopeq12  27962  ranksng  28174  neibastop3  28554  tailval  28565  filnetlem4  28573  heiborlem3  28683  ismrer1  28708  mzpclval  29032  mzpcl1  29036  wopprc  29350  inisegn0  29367  dnnumch3lem  29370  aomclem8  29385  mapfien2OLD  29420  mendvsca  29519  cytpval  29548  dvconstbi  29579  otiunsndisj  30103  f12dfv  30117  f13dfv  30118  usgra2pthlem1  30271  frgraunss  30558  frgra1v  30561  frgra2v  30562  frgra3v  30565  1vwmgra  30566  3vfriswmgra  30568  3cyclfrgrarn1  30575  n4cyclfrgra  30581  frgrancvvdeqlem4  30597  frgrawopreglem4  30611  frgraregorufr0  30616  2spotiundisj  30626  opeliun2xp  30690  dmmpt2ssx2  30697  lindslinindsimp2  30928  ldepspr  30938  ldepsnlinc  30981  bnj1373  31950  bnj1489  31976  lshpnel2N  32523  lsatlspsn2  32530  lsatlspsn  32531  lsatspn0  32538  lkrscss  32636  lfl1dim  32659  lfl1dim2N  32660  ldualvs  32675  atpointN  33280  watvalN  33530  trnsetN  33693  dih1dimatlem  34867  dihatexv  34876  dihjat1lem  34966  dihjat1  34967  lcfl7N  35039  lcfl8  35040  lcfl9a  35043  lcfrlem8  35087  lcfrlem9  35088  lcf1o  35089  mapdval2N  35168  mapdval4N  35170  mapdspex  35206  mapdn0  35207  mapdpglem23  35232  mapdpg  35244  mapdindp1  35258  mapdheq  35266  hvmapval  35298  mapdh9a  35328  hdmap1eq  35340  hdmap1cbv  35341  hdmapval  35369  hdmap10  35381  hdmaplkr  35454