Theorem sneq 4006

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 2437	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2558	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3997	. 2 |- { A } = { x | x = A }
4		df-sn 3997	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2488	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1437   {cab 2407   {csn 3996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-sn 3997

This theorem is referenced by:  sneqi  4007  sneqd  4008  euabsn  4069  absneu  4071  preq1  4076  tpeq3  4087  snssg  4130  sneqrg  4166  sneqbg  4167  opeq1  4184  unisng  4232  opthwiener  4719  otiunsndisj  4723  opeliunxp  4902  relop  5001  elimasng  5210  inisegn0  5216  xpdifid  5281  dmsnsnsn  5330  predeq123  5397  suceq  5504  iotajust  5561  fconstg  5784  f1osng  5866  opabiotafun  5939  fvn0ssdmfun  6025  fsng  6075  fsn2g  6076  fnressn  6088  fressnfv  6090  funfvima3  6154  f12dfv  6184  f13dfv  6185  isofrlem  6243  isoselem  6244  snnex  6608  elxp4  6748  elxp5  6749  1stval  6806  2ndval  6807  2ndval2  6822  fo1st  6824  fo2nd  6825  f1stres  6826  f2ndres  6827  mpt2mptsx  6867  dmmpt2ssx  6869  fmpt2x  6870  ovmptss  6885  fparlem3  6906  fparlem4  6907  suppval  6924  suppsnop  6936  ressuppssdif  6944  brtpos2  6984  dftpos4  6997  tpostpos  6998  eceq1  7404  fvdiagfn  7521  mapsncnv  7523  elixpsn  7566  ixpsnf1o  7567  ensn1g  7638  en1  7640  difsnen  7657  xpsneng  7660  xpcomco  7665  xpassen  7669  xpdom2  7670  canth2  7728  phplem3  7756  xpfi  7845  marypha2lem2  7953  cardsn  8405  pm54.43  8436  dfac5lem3  8557  dfac5lem4  8558  kmlem9  8589  kmlem11  8591  kmlem12  8592  ackbij1lem8  8658  r1om  8675  fictb  8676  hsmexlem4  8860  axcc2lem  8867  axcc2  8868  axdc3lem4  8884  fpwwe2cbv  9056  fpwwe2lem3  9059  fpwwecbv  9070  canth4  9073  fsum2dlem  13819  fsumcnv  13822  fsumcom2  13823  ackbijnn  13874  fprod2dlem  14022  fprodcnv  14025  fprodcom2  14026  lcmfunsnlem1  14598  lcmfunsnlem2lem1  14599  lcmfunsnlem2lem2  14600  lcmfunsnlem2  14601  lcmfunsn  14605  vdwlem1  14919  vdwlem12  14930  vdwlem13  14931  vdwnn  14936  0ram  14966  ramz2  14970  pwsval  15372  xpsfval  15461  xpsval  15466  symg2bas  17027  symgfixelsi  17064  pmtrfv  17081  pmtrprfval  17116  sylow2a  17259  efgrelexlema  17387  gsum2dlem2  17591  gsum2d2  17594  gsumcom2  17595  dprdcntz  17628  dprddisj  17629  dprd2dlem2  17661  dprd2dlem1  17662  dprd2da  17663  ablfac1eu  17694  ablfaclem3  17708  lssats2  18211  lspsneq0  18223  lbsind  18291  lspsneq  18333  lspdisj2  18338  lspsnsubn0  18351  lspprat  18364  islbs2  18365  lbsextlem4  18372  lbsextg  18373  lpi0  18459  lpi1  18460  psrvsca  18603  evlssca  18733  mpfind  18747  coe1fv  18787  coe1tm  18854  pf1ind  18931  frlmlbs  19342  lindfind  19361  lindsind  19362  lindfrn  19366  submaval  19593  mdetunilem3  19626  mdetunilem4  19627  mdetunilem9  19632  islp  20143  perfi  20158  t1sncld  20329  bwth  20412  dis2ndc  20462  nllyi  20477  dissnlocfin  20531  ptbasfi  20583  txkgen  20654  xkofvcn  20686  xkoinjcn  20689  qtopeu  20718  txswaphmeolem  20806  pt1hmeo  20808  elflim2  20966  cnextfvval  21067  cnextcn  21069  cnextfres1  21070  cnextfres  21071  tsmsxplem1  21154  tsmsxplem2  21155  ucncn  21287  itg11  22636  i1faddlem  22638  i1fmullem  22639  itg1addlem3  22643  itg1mulc  22649  eldv  22840  ply1lpir  23123  areambl  23871  tglngval  24583  nbgraopALT  25138  nb3graprlem2  25166  cusgrarn  25173  cusgra1v  25175  cusgra2v  25176  cusgra3v  25178  cusgrares  25186  usgrasscusgra  25197  sizeusglecusglem1  25198  uvtxel  25203  cusgrauvtxb  25210  vdgrval  25610  frgraunss  25709  frgra1v  25712  frgra2v  25713  frgra3v  25716  1vwmgra  25717  3vfriswmgra  25719  3cyclfrgrarn1  25726  n4cyclfrgra  25732  frgrancvvdeqlem4  25747  frgrawopreglem4  25761  frgraregorufr0  25766  2spotiundisj  25776  gxval  25972  h1de2ctlem  27194  spansn  27198  elspansn  27205  elspansn2  27206  spansneleq  27209  h1datom  27221  spansnj  27286  spansncv  27292  superpos  27993  sumdmdlem2  28058  aciunf1lem  28254  dfcnv2  28269  gsummpt2co  28538  locfinreflem  28663  esum2dlem  28909  sibfima  29167  sibfof  29169  bnj1373  29835  bnj1489  29861  cvmscbv  29977  cvmsdisj  29989  cvmsss2  29993  cvmliftlem15  30017  cvmlift2lem11  30032  cvmlift2lem12  30033  cvmlift2lem13  30034  mvtinf  30189  eldm3  30397  elima4  30416  fvsingle  30680  snelsingles  30682  dfiota3  30683  brapply  30698  funpartlem  30702  altopeq12  30722  ranksng  30927  neibastop3  31011  tailval  31022  filnetlem4  31030  f1omptsnlem  31679  f1omptsn  31680  mptsnun  31682  dissneqlem  31683  dissneq  31684  poimirlem4  31858  poimirlem25  31879  poimirlem26  31880  poimirlem27  31881  poimirlem31  31885  poimirlem32  31886  heiborlem3  32059  ismrer1  32084  lshpnel2N  32470  lsatlspsn2  32477  lsatlspsn  32478  lsatspn0  32485  lkrscss  32583  lfl1dim  32606  lfl1dim2N  32607  ldualvs  32622  atpointN  33227  watvalN  33477  trnsetN  33641  dih1dimatlem  34816  dihatexv  34825  dihjat1lem  34915  dihjat1  34916  lcfl7N  34988  lcfl8  34989  lcfl9a  34992  lcfrlem8  35036  lcfrlem9  35037  lcf1o  35038  mapdval2N  35117  mapdval4N  35119  mapdspex  35155  mapdn0  35156  mapdpglem23  35181  mapdpg  35193  mapdindp1  35207  mapdheq  35215  hvmapval  35247  mapdh9a  35277  hdmap1eq  35289  hdmap1cbv  35290  hdmapval  35318  hdmap10  35330  hdmaplkr  35403  mzpclval  35486  mzpcl1  35490  wopprc  35805  dnnumch3lem  35824  aomclem8  35839  mendvsca  35977  cytpval  36006  dvconstbi  36541  wessf1ornlem  37309  dvmptfprodlem  37639  fourierdlem32  37822  fourierdlem33  37823  fourierdlem48  37838  fzopredsuc  38432  issn  38700  propeqop  38704  usgra2pthlem1  38939  irinitoringc  39343  opeliun2xp  39388  dmmpt2ssx2  39392  lindslinindsimp2  39530  ldepspr  39540  ldepsnlinc  39575