Theorem sneq 3977

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 2461	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2568	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3968	. 2 |- { A } = { x | x = A }
4		df-sn 3968	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2509	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1443   {cab 2436   {csn 3967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-sn 3968

This theorem is referenced by:  sneqi  3978  sneqd  3979  euabsn  4043  absneu  4045  preq1  4050  tpeq3  4061  snssg  4104  sneqrg  4140  sneqbg  4141  opeq1  4165  unisng  4213  opthwiener  4702  otiunsndisj  4706  opeliunxp  4885  relop  4984  elimasng  5193  inisegn0  5199  xpdifid  5264  dmsnsnsn  5313  predeq123  5380  suceq  5487  iotajust  5544  fconstg  5768  f1osng  5851  opabiotafun  5924  fvn0ssdmfun  6011  fsng  6061  fsn2g  6062  fnressn  6074  fressnfv  6076  funfvima3  6140  f12dfv  6170  f13dfv  6171  isofrlem  6229  isoselem  6230  snnex  6594  elxp4  6734  elxp5  6735  1stval  6792  2ndval  6793  2ndval2  6808  fo1st  6810  fo2nd  6811  f1stres  6812  f2ndres  6813  mpt2mptsx  6853  dmmpt2ssx  6855  fmpt2x  6856  ovmptss  6874  fparlem3  6895  fparlem4  6896  suppval  6913  suppsnop  6925  ressuppssdif  6933  brtpos2  6976  dftpos4  6989  tpostpos  6990  eceq1  7396  fvdiagfn  7513  mapsncnv  7515  elixpsn  7558  ixpsnf1o  7559  ensn1g  7631  en1  7633  difsnen  7651  xpsneng  7654  xpcomco  7659  xpassen  7663  xpdom2  7664  canth2  7722  phplem3  7750  xpfi  7839  marypha2lem2  7947  cardsn  8400  pm54.43  8431  dfac5lem3  8553  dfac5lem4  8554  kmlem9  8585  kmlem11  8587  kmlem12  8588  ackbij1lem8  8654  r1om  8671  fictb  8672  hsmexlem4  8856  axcc2lem  8863  axcc2  8864  axdc3lem4  8880  fpwwe2cbv  9052  fpwwe2lem3  9055  fpwwecbv  9066  canth4  9069  fsum2dlem  13824  fsumcnv  13827  fsumcom2  13828  ackbijnn  13879  fprod2dlem  14027  fprodcnv  14030  fprodcom2  14031  lcmfunsnlem1  14603  lcmfunsnlem2lem1  14604  lcmfunsnlem2lem2  14605  lcmfunsnlem2  14606  lcmfunsn  14610  vdwlem1  14924  vdwlem12  14935  vdwlem13  14936  vdwnn  14941  0ram  14971  ramz2  14975  pwsval  15377  xpsfval  15466  xpsval  15471  symg2bas  17032  symgfixelsi  17069  pmtrfv  17086  pmtrprfval  17121  sylow2a  17264  efgrelexlema  17392  gsum2dlem2  17596  gsum2d2  17599  gsumcom2  17600  dprdcntz  17633  dprddisj  17634  dprd2dlem2  17666  dprd2dlem1  17667  dprd2da  17668  ablfac1eu  17699  ablfaclem3  17713  lssats2  18216  lspsneq0  18228  lbsind  18296  lspsneq  18338  lspdisj2  18343  lspsnsubn0  18356  lspprat  18369  islbs2  18370  lbsextlem4  18377  lbsextg  18378  lpi0  18464  lpi1  18465  psrvsca  18608  evlssca  18738  mpfind  18752  coe1fv  18792  coe1tm  18859  pf1ind  18936  frlmlbs  19348  lindfind  19367  lindsind  19368  lindfrn  19372  submaval  19599  mdetunilem3  19632  mdetunilem4  19633  mdetunilem9  19638  islp  20149  perfi  20164  t1sncld  20335  bwth  20418  dis2ndc  20468  nllyi  20483  dissnlocfin  20537  ptbasfi  20589  txkgen  20660  xkofvcn  20692  xkoinjcn  20695  qtopeu  20724  txswaphmeolem  20812  pt1hmeo  20814  elflim2  20972  cnextfvval  21073  cnextcn  21075  cnextfres1  21076  cnextfres  21077  tsmsxplem1  21160  tsmsxplem2  21161  ucncn  21293  itg11  22642  i1faddlem  22644  i1fmullem  22645  itg1addlem3  22649  itg1mulc  22655  eldv  22846  ply1lpir  23129  areambl  23877  tglngval  24589  nbgraopALT  25145  nb3graprlem2  25173  cusgrarn  25180  cusgra1v  25182  cusgra2v  25183  cusgra3v  25185  cusgrares  25193  usgrasscusgra  25204  sizeusglecusglem1  25205  uvtxel  25210  cusgrauvtxb  25217  vdgrval  25617  frgraunss  25716  frgra1v  25719  frgra2v  25720  frgra3v  25723  1vwmgra  25724  3vfriswmgra  25726  3cyclfrgrarn1  25733  n4cyclfrgra  25739  frgrancvvdeqlem4  25754  frgrawopreglem4  25768  frgraregorufr0  25773  2spotiundisj  25783  gxval  25979  h1de2ctlem  27201  spansn  27205  elspansn  27212  elspansn2  27213  spansneleq  27216  h1datom  27228  spansnj  27293  spansncv  27299  superpos  28000  sumdmdlem2  28065  aciunf1lem  28257  dfcnv2  28272  gsummpt2co  28536  locfinreflem  28660  esum2dlem  28906  sibfima  29164  sibfof  29166  bnj1373  29832  bnj1489  29858  cvmscbv  29974  cvmsdisj  29986  cvmsss2  29990  cvmliftlem15  30014  cvmlift2lem11  30029  cvmlift2lem12  30030  cvmlift2lem13  30031  mvtinf  30186  eldm3  30395  elima4  30414  fvsingle  30680  snelsingles  30682  dfiota3  30683  brapply  30698  funpartlem  30702  altopeq12  30722  ranksng  30927  neibastop3  31011  tailval  31022  filnetlem4  31030  f1omptsnlem  31731  f1omptsn  31732  mptsnun  31734  dissneqlem  31735  dissneq  31736  poimirlem4  31937  poimirlem25  31958  poimirlem26  31959  poimirlem27  31960  poimirlem31  31964  poimirlem32  31965  heiborlem3  32138  ismrer1  32163  lshpnel2N  32545  lsatlspsn2  32552  lsatlspsn  32553  lsatspn0  32560  lkrscss  32658  lfl1dim  32681  lfl1dim2N  32682  ldualvs  32697  atpointN  33302  watvalN  33552  trnsetN  33716  dih1dimatlem  34891  dihatexv  34900  dihjat1lem  34990  dihjat1  34991  lcfl7N  35063  lcfl8  35064  lcfl9a  35067  lcfrlem8  35111  lcfrlem9  35112  lcf1o  35113  mapdval2N  35192  mapdval4N  35194  mapdspex  35230  mapdn0  35231  mapdpglem23  35256  mapdpg  35268  mapdindp1  35282  mapdheq  35290  hvmapval  35322  mapdh9a  35352  hdmap1eq  35364  hdmap1cbv  35365  hdmapval  35393  hdmap10  35405  hdmaplkr  35478  mzpclval  35561  mzpcl1  35565  wopprc  35879  dnnumch3lem  35898  aomclem8  35913  mendvsca  36051  cytpval  36080  dvconstbi  36677  wessf1ornlem  37453  dvmptfprodlem  37813  fourierdlem32  37996  fourierdlem33  37997  fourierdlem48  38012  fzopredsuc  38714  issn  38989  propeqop  38993  nbgrval  39389  nbgr2vtx1edg  39401  nbuhgr2vtx1edgb  39403  nbgr1vtx  39409  nb3grprlem2  39438  uvtxael  39443  uvtxael1  39451  uvtxusgrel  39459  cusgredg  39475  cplgr1v  39480  cplgr3v  39485  usgredgsscusgredg  39503  vtxdgval  39512  uspgrloopvd2  39540  1wlk1walk  39630  usgra2pthlem1  39654  irinitoringc  40058  opeliun2xp  40101  dmmpt2ssx2  40105  lindslinindsimp2  40243  ldepspr  40253  ldepsnlinc  40288