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

Theorem sneq 3664
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 2305 . . 3  |-  ( A  =  B  ->  (
x  =  A  <->  x  =  B ) )
21abbidv 2410 . 2  |-  ( A  =  B  ->  { x  |  x  =  A }  =  { x  |  x  =  B } )
3 df-sn 3659 . 2  |-  { A }  =  { x  |  x  =  A }
4 df-sn 3659 . 2  |-  { B }  =  { x  |  x  =  B }
52, 3, 43eqtr4g 2353 1  |-  ( A  =  B  ->  { A }  =  { B } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   {cab 2282   {csn 3653
This theorem is referenced by:  sneqi  3665  sneqd  3666  euabsn  3712  absneu  3714  preq1  3719  tpeq3  3730  snssg  3767  sneqrg  3798  sneqbg  3799  opeq1  3812  unisng  3860  opthwiener  4284  suceq  4473  snnex  4540  opeliunxp  4756  relop  4850  elimasng  5055  dmsnsnsn  5167  elxp4  5176  elxp5  5177  iotajust  5234  fconstg  5444  f1osng  5530  fsng  5713  fnressn  5721  fressnfv  5723  funfvima3  5771  isofrlem  5853  isoselem  5854  1stval  6140  2ndval  6141  2ndval2  6154  fo1st  6155  fo2nd  6156  f1stres  6157  f2ndres  6158  mpt2mptsx  6203  dmmpt2ssx  6205  fmpt2x  6206  ovmptss  6216  fparlem3  6236  fparlem4  6237  brtpos2  6256  dftpos4  6269  tpostpos  6270  opabiotafun  6307  eceq1  6712  fvdiagfn  6828  mapsncnv  6830  elixpsn  6871  ixpsnf1o  6872  ensn1g  6942  en1  6944  difsnen  6960  xpsneng  6963  xpcomco  6968  xpassen  6972  xpdom2  6973  canth2  7030  phplem3  7058  xpfi  7144  marypha2lem2  7205  cardsn  7618  pm54.43  7649  dfac5lem3  7768  dfac5lem4  7769  kmlem9  7800  kmlem11  7802  kmlem12  7803  ackbij1lem8  7869  r1om  7886  fictb  7887  hsmexlem4  8071  axcc2lem  8078  axcc2  8079  axdc3lem4  8095  fpwwe2cbv  8268  fpwwe2lem3  8271  fpwwecbv  8282  canth4  8285  fsum2dlem  12249  fsumcnv  12252  fsumcom2  12253  ackbijnn  12302  xpnnenOLD  12504  vdwlem1  13044  vdwlem12  13055  vdwlem13  13056  vdwnn  13061  0ram  13083  ramz2  13087  pwsval  13401  xpsfval  13485  xpsval  13490  sylow2a  14946  efgrelexlema  15074  gsum2d  15239  gsum2d2  15241  gsumcom2  15242  dprdcntz  15259  dprddisj  15260  dprd2dlem2  15291  dprd2dlem1  15292  dprd2da  15293  ablfac1eu  15324  ablfaclem3  15338  lssats2  15773  lspsneq0  15785  lbsind  15849  lspsneq  15891  lspdisj2  15896  lspsnsubn0  15909  lspprat  15922  islbs2  15923  lbsextlem4  15930  lbsextg  15931  lpi0  16015  lpi1  16016  psrvsca  16152  coe1fv  16303  coe1tm  16365  islp  16888  perfi  16902  t1sncld  17070  dis2ndc  17202  nllyi  17217  ptbasfi  17292  txkgen  17362  xkofvcn  17394  xkoinjcn  17397  qtopeu  17423  txswaphmeolem  17511  pt1hmeo  17513  elflim2  17675  tsmsxplem1  17851  tsmsxplem2  17852  itg11  19062  i1faddlem  19064  i1fmullem  19065  itg1addlem3  19069  itg1mulc  19075  eldv  19264  evlssca  19422  mpfind  19444  pf1ind  19454  ply1lpir  19580  areambl  20269  gxval  20941  h1de2ctlem  22150  spansn  22154  elspansn  22161  elspansn2  22162  spansneleq  22165  h1datom  22177  spansnj  22242  spansncv  22248  superpos  22950  sumdmdlem2  23015  cvmscbv  23804  cvmsdisj  23816  cvmsss2  23820  cvmliftlem15  23844  cvmlift2lem11  23859  cvmlift2lem12  23860  cvmlift2lem13  23861  vdgrval  23905  eldm3  24190  predeq3  24242  fvsingle  24530  snelsingles  24532  dfiota3  24533  brapply  24548  funpartlem  24552  altopeq12  24568  ranksng  24869  itg2addnclem  25003  itg2addnc  25005  fatesg  25059  snelpwg  25194  cbicp  25269  valcurfn1  25307  osneisi  25634  islimrs  25683  isder  25810  valtar  25986  lineval222  26182  lineval3a  26186  sgplpte21  26235  sgplpte22  26241  isray2  26256  isray  26257  neibastop3  26414  tailval  26425  filnetlem4  26433  heiborlem3  26640  ismrer1  26665  mzpclval  26906  mzpcl1  26910  wopprc  27226  inisegn0  27243  dnnumch3lem  27246  aomclem8  27262  frlmlbs  27352  mapfien2  27361  lindfind  27389  lindsind  27390  lindfrn  27394  pmtrfv  27498  mendvsca  27602  cytpval  27631  dvconstbi  27654  nb3graprlem2  28288  cusgra1v  28296  cusgra2v  28297  cusgra3v  28299  uvtxel  28302  uvtxisvtx  28303  cusgrauvtx  28309  frgra1v  28422  frgra2v  28423  frgra3v  28426  1vwmgra  28427  3vfriswmgra  28429  3cyclfrgrarn1  28435  n4cyclfrgra  28440  bnj1373  29376  bnj1489  29402  lshpnel2N  29797  lsatlspsn2  29804  lsatlspsn  29805  lsatspn0  29812  lkrscss  29910  lfl1dim  29933  lfl1dim2N  29934  ldualvs  29949  atpointN  30554  watvalN  30804  trnsetN  30967  dih1dimatlem  32141  dihatexv  32150  dihjat1lem  32240  dihjat1  32241  lcfl7N  32313  lcfl8  32314  lcfl9a  32317  lcfrlem8  32361  lcfrlem9  32362  lcf1o  32363  mapdval2N  32442  mapdval4N  32444  mapdspex  32480  mapdn0  32481  mapdpglem23  32506  mapdpg  32518  mapdindp1  32532  mapdheq  32540  hvmapval  32572  mapdh9a  32602  hdmap1eq  32614  hdmap1cbv  32615  hdmapval  32643  hdmap10  32655  hdmaplkr  32728
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-sn 3659
  Copyright terms: Public domain W3C validator