MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sneq Unicode version

Theorem sneq 3651
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.
StepHypRef Expression
1 eqeq2 2292 . . 3  |-  ( A  =  B  ->  (
x  =  A  <->  x  =  B ) )
21abbidv 2397 . 2  |-  ( A  =  B  ->  { x  |  x  =  A }  =  { x  |  x  =  B } )
3 df-sn 3646 . 2  |-  { A }  =  { x  |  x  =  A }
4 df-sn 3646 . 2  |-  { B }  =  { x  |  x  =  B }
52, 3, 43eqtr4g 2340 1  |-  ( A  =  B  ->  { A }  =  { B } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   {cab 2269   {csn 3640
This theorem is referenced by:  sneqi  3652  sneqd  3653  euabsn  3699  absneu  3701  preq1  3706  tpeq3  3717  snssg  3754  sneqrg  3782  sneqbg  3783  opeq1  3796  unisng  3844  opthwiener  4268  suceq  4457  snnex  4524  opeliunxp  4740  relop  4834  elimasng  5039  dmsnsnsn  5151  elxp4  5160  elxp5  5161  iotajust  5218  fconstg  5428  f1osng  5514  fsng  5697  fnressn  5705  fressnfv  5707  funfvima3  5755  isofrlem  5837  isoselem  5838  1stval  6124  2ndval  6125  2ndval2  6138  fo1st  6139  fo2nd  6140  f1stres  6141  f2ndres  6142  mpt2mptsx  6187  dmmpt2ssx  6189  fmpt2x  6190  ovmptss  6200  fparlem3  6220  fparlem4  6221  brtpos2  6240  dftpos4  6253  tpostpos  6254  opabiotafun  6291  eceq1  6696  fvdiagfn  6812  mapsncnv  6814  elixpsn  6855  ixpsnf1o  6856  ensn1g  6926  en1  6928  difsnen  6944  xpsneng  6947  xpcomco  6952  xpassen  6956  xpdom2  6957  canth2  7014  phplem3  7042  xpfi  7128  marypha2lem2  7189  cardsn  7602  pm54.43  7633  dfac5lem3  7752  dfac5lem4  7753  kmlem9  7784  kmlem11  7786  kmlem12  7787  ackbij1lem8  7853  r1om  7870  fictb  7871  hsmexlem4  8055  axcc2lem  8062  axcc2  8063  axdc3lem4  8079  fpwwe2cbv  8252  fpwwe2lem3  8255  fpwwecbv  8266  canth4  8269  fsum2dlem  12233  fsumcnv  12236  fsumcom2  12237  ackbijnn  12286  xpnnenOLD  12488  vdwlem1  13028  vdwlem12  13039  vdwlem13  13040  vdwnn  13045  0ram  13067  ramz2  13071  pwsval  13385  xpsfval  13469  xpsval  13474  sylow2a  14930  efgrelexlema  15058  gsum2d  15223  gsum2d2  15225  gsumcom2  15226  dprdcntz  15243  dprddisj  15244  dprd2dlem2  15275  dprd2dlem1  15276  dprd2da  15277  ablfac1eu  15308  ablfaclem3  15322  lssats2  15757  lspsneq0  15769  lbsind  15833  lspsneq  15875  lspdisj2  15880  lspsnsubn0  15893  lspprat  15906  islbs2  15907  lbsextlem4  15914  lbsextg  15915  lpi0  15999  lpi1  16000  psrvsca  16136  coe1fv  16287  coe1tm  16349  islp  16872  perfi  16886  t1sncld  17054  dis2ndc  17186  nllyi  17201  ptbasfi  17276  txkgen  17346  xkofvcn  17378  xkoinjcn  17381  qtopeu  17407  txswaphmeolem  17495  pt1hmeo  17497  elflim2  17659  tsmsxplem1  17835  tsmsxplem2  17836  itg11  19046  i1faddlem  19048  i1fmullem  19049  itg1addlem3  19053  itg1mulc  19059  eldv  19248  evlssca  19406  mpfind  19428  pf1ind  19438  ply1lpir  19564  areambl  20253  gxval  20925  h1de2ctlem  22134  spansn  22138  elspansn  22145  elspansn2  22146  spansneleq  22149  h1datom  22161  spansnj  22226  spansncv  22232  superpos  22934  sumdmdlem2  22999  cvmscbv  23789  cvmsdisj  23801  cvmsss2  23805  cvmliftlem15  23829  cvmlift2lem11  23844  cvmlift2lem12  23845  cvmlift2lem13  23846  vdgrval  23890  eldm3  24119  predeq3  24171  fvsingle  24459  snelsingles  24461  dfiota3  24462  brapply  24477  funpartfv  24483  altopeq12  24496  ranksng  24797  fatesg  24956  snelpwg  25091  cbicp  25166  valcurfn1  25204  osneisi  25531  islimrs  25580  isder  25707  valtar  25883  lineval222  26079  lineval3a  26083  sgplpte21  26132  sgplpte22  26138  isray2  26153  isray  26154  neibastop3  26311  tailval  26322  filnetlem4  26330  heiborlem3  26537  ismrer1  26562  mzpclval  26803  mzpcl1  26807  wopprc  27123  inisegn0  27140  dnnumch3lem  27143  aomclem8  27159  frlmlbs  27249  mapfien2  27258  lindfind  27286  lindsind  27287  lindfrn  27291  pmtrfv  27395  mendvsca  27499  cytpval  27528  dvconstbi  27551  cusgra1v  28157  cusgra2v  28158  uvtxel  28161  uvtxisvtx  28162  cusgrauvtx  28168  frgra1v  28176  frgra2v  28177  frgra3v  28180  1vwmgra  28181  3vfriswmgra  28183  bnj1373  29060  bnj1489  29086  lshpnel2N  29175  lsatlspsn2  29182  lsatlspsn  29183  lsatspn0  29190  lkrscss  29288  lfl1dim  29311  lfl1dim2N  29312  ldualvs  29327  atpointN  29932  watvalN  30182  trnsetN  30345  dih1dimatlem  31519  dihatexv  31528  dihjat1lem  31618  dihjat1  31619  lcfl7N  31691  lcfl8  31692  lcfl9a  31695  lcfrlem8  31739  lcfrlem9  31740  lcf1o  31741  mapdval2N  31820  mapdval4N  31822  mapdspex  31858  mapdn0  31859  mapdpglem23  31884  mapdpg  31896  mapdindp1  31910  mapdheq  31918  hvmapval  31950  mapdh9a  31980  hdmap1eq  31992  hdmap1cbv  31993  hdmapval  32021  hdmap10  32033  hdmaplkr  32106
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-sn 3646
  Copyright terms: Public domain W3C validator