Theorem sneq 3982

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 2417	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2538	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3973	. 2 |- { A } = { x | x = A }
4		df-sn 3973	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2468	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1405   {cab 2387   {csn 3972

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-sn 3973

This theorem is referenced by:  sneqi  3983  sneqd  3984  euabsn  4044  absneu  4046  preq1  4051  tpeq3  4062  snssg  4105  sneqrg  4141  sneqbg  4142  opeq1  4159  unisng  4207  opthwiener  4692  otiunsndisj  4696  opeliunxp  4875  relop  4974  elimasng  5183  xpdifid  5253  dmsnsnsn  5302  predeq123  5368  suceq  5475  iotajust  5532  fconstg  5755  f1osng  5837  opabiotafun  5910  fvn0ssdmfun  6000  fsng  6050  fsn2g  6051  fnressn  6063  fressnfv  6065  funfvima3  6130  f12dfv  6160  f13dfv  6161  isofrlem  6219  isoselem  6220  snnex  6588  elxp4  6728  elxp5  6729  1stval  6786  2ndval  6787  2ndval2  6802  fo1st  6804  fo2nd  6805  f1stres  6806  f2ndres  6807  mpt2mptsx  6847  dmmpt2ssx  6849  fmpt2x  6850  ovmptss  6865  fparlem3  6886  fparlem4  6887  suppval  6904  suppsnop  6916  ressuppssdif  6924  brtpos2  6964  dftpos4  6977  tpostpos  6978  eceq1  7384  fvdiagfn  7501  mapsncnv  7503  elixpsn  7546  ixpsnf1o  7547  ensn1g  7618  en1  7620  difsnen  7637  xpsneng  7640  xpcomco  7645  xpassen  7649  xpdom2  7650  canth2  7708  phplem3  7736  xpfi  7825  marypha2lem2  7930  cardsn  8382  pm54.43  8413  dfac5lem3  8538  dfac5lem4  8539  kmlem9  8570  kmlem11  8572  kmlem12  8573  ackbij1lem8  8639  r1om  8656  fictb  8657  hsmexlem4  8841  axcc2lem  8848  axcc2  8849  axdc3lem4  8865  fpwwe2cbv  9038  fpwwe2lem3  9041  fpwwecbv  9052  canth4  9055  fsum2dlem  13736  fsumcnv  13739  fsumcom2  13740  ackbijnn  13791  fprod2dlem  13936  fprodcnv  13939  fprodcom2  13940  vdwlem1  14708  vdwlem12  14719  vdwlem13  14720  vdwnn  14725  0ram  14747  ramz2  14751  pwsval  15100  xpsfval  15181  xpsval  15186  symg2bas  16747  symgfixelsi  16784  pmtrfv  16801  pmtrprfval  16836  sylow2a  16963  efgrelexlema  17091  gsum2dlem2  17319  gsum2dOLD  17321  gsum2d2  17323  gsumcom2  17324  dprdcntz  17361  dprddisj  17362  dprd2dlem2  17409  dprd2dlem1  17410  dprd2da  17411  ablfac1eu  17444  ablfaclem3  17458  lssats2  17966  lspsneq0  17978  lbsind  18046  lspsneq  18088  lspdisj2  18093  lspsnsubn0  18106  lspprat  18119  islbs2  18120  lbsextlem4  18127  lbsextg  18128  lpi0  18215  lpi1  18216  psrvsca  18364  evlssca  18511  mpfind  18525  coe1fv  18565  coe1tm  18634  pf1ind  18711  frlmlbs  19124  lindfind  19143  lindsind  19144  lindfrn  19148  submaval  19375  mdetunilem3  19408  mdetunilem4  19409  mdetunilem9  19414  islp  19934  perfi  19949  t1sncld  20120  bwth  20203  dis2ndc  20253  nllyi  20268  dissnlocfin  20322  ptbasfi  20374  txkgen  20445  xkofvcn  20477  xkoinjcn  20480  qtopeu  20509  txswaphmeolem  20597  pt1hmeo  20599  elflim2  20757  cnextfvval  20857  cnextcn  20859  cnextfres  20860  tsmsxplem1  20947  tsmsxplem2  20948  ucncn  21080  itg11  22390  i1faddlem  22392  i1fmullem  22393  itg1addlem3  22397  itg1mulc  22403  eldv  22594  ply1lpir  22871  areambl  23614  tglngval  24321  nbgraopALT  24841  nb3graprlem2  24869  cusgrarn  24876  cusgra1v  24878  cusgra2v  24879  cusgra3v  24881  cusgrares  24889  usgrasscusgra  24900  sizeusglecusglem1  24901  uvtxel  24906  cusgrauvtxb  24913  vdgrval  25313  frgraunss  25412  frgra1v  25415  frgra2v  25416  frgra3v  25419  1vwmgra  25420  3vfriswmgra  25422  3cyclfrgrarn1  25429  n4cyclfrgra  25435  frgrancvvdeqlem4  25450  frgrawopreglem4  25464  frgraregorufr0  25469  2spotiundisj  25479  gxval  25674  h1de2ctlem  26887  spansn  26891  elspansn  26898  elspansn2  26899  spansneleq  26902  h1datom  26914  spansnj  26979  spansncv  26985  superpos  27686  sumdmdlem2  27751  aciunf1lem  27946  dfcnv2  27961  gsummpt2co  28222  locfinreflem  28296  esum2dlem  28539  sibfima  28786  sibfof  28788  bnj1373  29413  bnj1489  29439  cvmscbv  29555  cvmsdisj  29567  cvmsss2  29571  cvmliftlem15  29595  cvmlift2lem11  29610  cvmlift2lem12  29611  cvmlift2lem13  29612  mvtinf  29767  eldm3  29975  elima4  29994  fvsingle  30258  snelsingles  30260  dfiota3  30261  brapply  30276  funpartlem  30280  altopeq12  30300  ranksng  30505  neibastop3  30590  tailval  30601  filnetlem4  30609  f1omptsnlem  31252  f1omptsn  31253  mptsnun  31255  dissneqlem  31256  dissneq  31257  heiborlem3  31591  ismrer1  31616  lshpnel2N  32003  lsatlspsn2  32010  lsatlspsn  32011  lsatspn0  32018  lkrscss  32116  lfl1dim  32139  lfl1dim2N  32140  ldualvs  32155  atpointN  32760  watvalN  33010  trnsetN  33174  dih1dimatlem  34349  dihatexv  34358  dihjat1lem  34448  dihjat1  34449  lcfl7N  34521  lcfl8  34522  lcfl9a  34525  lcfrlem8  34569  lcfrlem9  34570  lcf1o  34571  mapdval2N  34650  mapdval4N  34652  mapdspex  34688  mapdn0  34689  mapdpglem23  34714  mapdpg  34726  mapdindp1  34740  mapdheq  34748  hvmapval  34780  mapdh9a  34810  hdmap1eq  34822  hdmap1cbv  34823  hdmapval  34851  hdmap10  34863  hdmaplkr  34936  mzpclval  35019  mzpcl1  35023  wopprc  35334  inisegn0  35351  dnnumch3lem  35354  aomclem8  35369  mapfien2OLD  35404  mendvsca  35504  cytpval  35533  dvconstbi  36087  dvmptfprodlem  37109  fourierdlem32  37289  fourierdlem33  37290  fourierdlem48  37305  fzopredsuc  37671  usgra2pthlem1  37982  irinitoringc  38388  opeliun2xp  38433  dmmpt2ssx2  38437  lindslinindsimp2  38575  ldepspr  38585  ldepsnlinc  38620