Theorem sneq 3785

Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-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 2413	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2518	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3780	. 2 |- { A } = { x | x = A }
4		df-sn 3780	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2461	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1649   {cab 2390   {csn 3774

This theorem is referenced by:  sneqi  3786  sneqd  3787  euabsn  3836  absneu  3838  preq1  3843  tpeq3  3854  snssg  3892  sneqrg  3928  sneqbg  3929  opeq1  3944  unisng  3992  opthwiener  4418  suceq  4606  snnex  4672  opeliunxp  4888  relop  4982  elimasng  5189  dmsnsnsn  5307  elxp4  5316  elxp5  5317  iotajust  5376  fconstg  5589  f1osng  5675  fsng  5866  fnressn  5877  fressnfv  5879  funfvima3  5934  isofrlem  6019  isoselem  6020  1stval  6310  2ndval  6311  2ndval2  6324  fo1st  6325  fo2nd  6326  f1stres  6327  f2ndres  6328  mpt2mptsx  6373  dmmpt2ssx  6375  fmpt2x  6376  ovmptss  6387  fparlem3  6407  fparlem4  6408  brtpos2  6444  dftpos4  6457  tpostpos  6458  opabiotafun  6495  eceq1  6900  fvdiagfn  7017  mapsncnv  7019  elixpsn  7060  ixpsnf1o  7061  ensn1g  7131  en1  7133  difsnen  7149  xpsneng  7152  xpcomco  7157  xpassen  7161  xpdom2  7162  canth2  7219  phplem3  7247  xpfi  7337  marypha2lem2  7399  cardsn  7812  pm54.43  7843  dfac5lem3  7962  dfac5lem4  7963  kmlem9  7994  kmlem11  7996  kmlem12  7997  ackbij1lem8  8063  r1om  8080  fictb  8081  hsmexlem4  8265  axcc2lem  8272  axcc2  8273  axdc3lem4  8289  fpwwe2cbv  8461  fpwwe2lem3  8464  fpwwecbv  8475  canth4  8478  fsum2dlem  12509  fsumcnv  12512  fsumcom2  12513  ackbijnn  12562  xpnnenOLD  12764  vdwlem1  13304  vdwlem12  13315  vdwlem13  13316  vdwnn  13321  0ram  13343  ramz2  13347  pwsval  13663  xpsfval  13747  xpsval  13752  sylow2a  15208  efgrelexlema  15336  gsum2d  15501  gsum2d2  15503  gsumcom2  15504  dprdcntz  15521  dprddisj  15522  dprd2dlem2  15553  dprd2dlem1  15554  dprd2da  15555  ablfac1eu  15586  ablfaclem3  15600  lssats2  16031  lspsneq0  16043  lbsind  16107  lspsneq  16149  lspdisj2  16154  lspsnsubn0  16167  lspprat  16180  islbs2  16181  lbsextlem4  16188  lbsextg  16189  lpi0  16273  lpi1  16274  psrvsca  16410  coe1fv  16559  coe1tm  16620  islp  17159  perfi  17173  t1sncld  17344  dis2ndc  17476  nllyi  17491  ptbasfi  17566  txkgen  17637  xkofvcn  17669  xkoinjcn  17672  qtopeu  17701  txswaphmeolem  17789  pt1hmeo  17791  elflim2  17949  cnextfvval  18049  cnextcn  18051  cnextfres  18052  tsmsxplem1  18135  tsmsxplem2  18136  ucncn  18268  itg11  19536  i1faddlem  19538  i1fmullem  19539  itg1addlem3  19543  itg1mulc  19549  eldv  19738  evlssca  19896  mpfind  19918  pf1ind  19928  ply1lpir  20054  areambl  20750  nb3graprlem2  21414  cusgrarn  21421  cusgra1v  21423  cusgra2v  21424  cusgra3v  21426  cusgrares  21434  usgrasscusgra  21445  sizeusglecusglem1  21446  uvtxel  21451  cusgrauvtxb  21458  vdgrval  21620  gxval  21799  h1de2ctlem  23010  spansn  23014  elspansn  23021  elspansn2  23022  spansneleq  23025  h1datom  23037  spansnj  23102  spansncv  23108  superpos  23810  sumdmdlem2  23875  sibfima  24606  sibfof  24607  cvmscbv  24898  cvmsdisj  24910  cvmsss2  24914  cvmliftlem15  24938  cvmlift2lem11  24953  cvmlift2lem12  24954  cvmlift2lem13  24955  fprod2dlem  25257  fprodcnv  25260  fprodcom2  25261  eldm3  25333  predeq3  25385  fvsingle  25673  snelsingles  25675  dfiota3  25676  brapply  25691  funpartlem  25695  altopeq12  25711  ranksng  26012  neibastop3  26281  tailval  26292  filnetlem4  26300  heiborlem3  26412  ismrer1  26437  mzpclval  26672  mzpcl1  26676  wopprc  26991  inisegn0  27008  dnnumch3lem  27011  aomclem8  27027  frlmlbs  27117  mapfien2  27126  lindfind  27154  lindsind  27155  lindfrn  27159  pmtrfv  27263  mendvsca  27367  cytpval  27396  dvconstbi  27419  otiunsndisj  27954  f12dfv  27961  f13dfv  27962  usgra2pthlem1  28040  frgraunss  28099  frgra1v  28102  frgra2v  28103  frgra3v  28106  1vwmgra  28107  3vfriswmgra  28109  3cyclfrgrarn1  28116  n4cyclfrgra  28122  frgrancvvdeqlem4  28136  frgrawopreglem4  28150  frgraregorufr0  28155  2spotiundisj  28165  bnj1373  29105  bnj1489  29131  lshpnel2N  29468  lsatlspsn2  29475  lsatlspsn  29476  lsatspn0  29483  lkrscss  29581  lfl1dim  29604  lfl1dim2N  29605  ldualvs  29620  atpointN  30225  watvalN  30475  trnsetN  30638  dih1dimatlem  31812  dihatexv  31821  dihjat1lem  31911  dihjat1  31912  lcfl7N  31984  lcfl8  31985  lcfl9a  31988  lcfrlem8  32032  lcfrlem9  32033  lcf1o  32034  mapdval2N  32113  mapdval4N  32115  mapdspex  32151  mapdn0  32152  mapdpglem23  32177  mapdpg  32189  mapdindp1  32203  mapdheq  32211  hvmapval  32243  mapdh9a  32273  hdmap1eq  32285  hdmap1cbv  32286  hdmapval  32314  hdmap10  32326  hdmaplkr  32399

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-sn 3780