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

Theorem sneq 3812
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 2439 . . 3  |-  ( A  =  B  ->  (
x  =  A  <->  x  =  B ) )
21abbidv 2544 . 2  |-  ( A  =  B  ->  { x  |  x  =  A }  =  { x  |  x  =  B } )
3 df-sn 3807 . 2  |-  { A }  =  { x  |  x  =  A }
4 df-sn 3807 . 2  |-  { B }  =  { x  |  x  =  B }
52, 3, 43eqtr4g 2487 1  |-  ( A  =  B  ->  { A }  =  { B } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   {cab 2416   {csn 3801
This theorem is referenced by:  sneqi  3813  sneqd  3814  euabsn  3863  absneu  3865  preq1  3870  tpeq3  3881  snssg  3919  sneqrg  3955  sneqbg  3956  opeq1  3971  unisng  4019  opthwiener  4445  suceq  4633  snnex  4699  opeliunxp  4915  relop  5009  elimasng  5216  dmsnsnsn  5334  elxp4  5343  elxp5  5344  iotajust  5403  fconstg  5616  f1osng  5702  fsng  5893  fnressn  5904  fressnfv  5906  funfvima3  5961  isofrlem  6046  isoselem  6047  1stval  6337  2ndval  6338  2ndval2  6351  fo1st  6352  fo2nd  6353  f1stres  6354  f2ndres  6355  mpt2mptsx  6400  dmmpt2ssx  6402  fmpt2x  6403  ovmptss  6414  fparlem3  6434  fparlem4  6435  brtpos2  6471  dftpos4  6484  tpostpos  6485  opabiotafun  6522  eceq1  6927  fvdiagfn  7044  mapsncnv  7046  elixpsn  7087  ixpsnf1o  7088  ensn1g  7158  en1  7160  difsnen  7176  xpsneng  7179  xpcomco  7184  xpassen  7188  xpdom2  7189  canth2  7246  phplem3  7274  xpfi  7364  marypha2lem2  7427  cardsn  7840  pm54.43  7871  dfac5lem3  7990  dfac5lem4  7991  kmlem9  8022  kmlem11  8024  kmlem12  8025  ackbij1lem8  8091  r1om  8108  fictb  8109  hsmexlem4  8293  axcc2lem  8300  axcc2  8301  axdc3lem4  8317  fpwwe2cbv  8489  fpwwe2lem3  8492  fpwwecbv  8503  canth4  8506  fsum2dlem  12537  fsumcnv  12540  fsumcom2  12541  ackbijnn  12590  xpnnenOLD  12792  vdwlem1  13332  vdwlem12  13343  vdwlem13  13344  vdwnn  13349  0ram  13371  ramz2  13375  pwsval  13691  xpsfval  13775  xpsval  13780  sylow2a  15236  efgrelexlema  15364  gsum2d  15529  gsum2d2  15531  gsumcom2  15532  dprdcntz  15549  dprddisj  15550  dprd2dlem2  15581  dprd2dlem1  15582  dprd2da  15583  ablfac1eu  15614  ablfaclem3  15628  lssats2  16059  lspsneq0  16071  lbsind  16135  lspsneq  16177  lspdisj2  16182  lspsnsubn0  16195  lspprat  16208  islbs2  16209  lbsextlem4  16216  lbsextg  16217  lpi0  16301  lpi1  16302  psrvsca  16438  coe1fv  16587  coe1tm  16648  islp  17187  perfi  17202  t1sncld  17373  dis2ndc  17506  nllyi  17521  ptbasfi  17596  txkgen  17667  xkofvcn  17699  xkoinjcn  17702  qtopeu  17731  txswaphmeolem  17819  pt1hmeo  17821  elflim2  17979  cnextfvval  18079  cnextcn  18081  cnextfres  18082  tsmsxplem1  18165  tsmsxplem2  18166  ucncn  18298  itg11  19566  i1faddlem  19568  i1fmullem  19569  itg1addlem3  19573  itg1mulc  19579  eldv  19768  evlssca  19926  mpfind  19948  pf1ind  19958  ply1lpir  20084  areambl  20780  nb3graprlem2  21444  cusgrarn  21451  cusgra1v  21453  cusgra2v  21454  cusgra3v  21456  cusgrares  21464  usgrasscusgra  21475  sizeusglecusglem1  21476  uvtxel  21481  cusgrauvtxb  21488  vdgrval  21650  gxval  21829  h1de2ctlem  23040  spansn  23044  elspansn  23051  elspansn2  23052  spansneleq  23055  h1datom  23067  spansnj  23132  spansncv  23138  superpos  23840  sumdmdlem2  23905  sibfima  24636  sibfof  24637  cvmscbv  24928  cvmsdisj  24940  cvmsss2  24944  cvmliftlem15  24968  cvmlift2lem11  24983  cvmlift2lem12  24984  cvmlift2lem13  24985  fprod2dlem  25288  fprodcnv  25291  fprodcom2  25292  eldm3  25369  predeq3  25421  fvsingle  25710  snelsingles  25712  dfiota3  25713  brapply  25728  funpartlem  25732  altopeq12  25750  ranksng  26051  neibastop3  26323  tailval  26334  filnetlem4  26342  heiborlem3  26454  ismrer1  26479  mzpclval  26714  mzpcl1  26718  wopprc  27033  inisegn0  27050  dnnumch3lem  27053  aomclem8  27069  frlmlbs  27159  mapfien2  27168  lindfind  27196  lindsind  27197  lindfrn  27201  pmtrfv  27305  mendvsca  27409  cytpval  27438  dvconstbi  27461  otiunsndisj  27996  f12dfv  28003  f13dfv  28004  usgra2pthlem1  28082  frgraunss  28141  frgra1v  28144  frgra2v  28145  frgra3v  28148  1vwmgra  28149  3vfriswmgra  28151  3cyclfrgrarn1  28158  n4cyclfrgra  28164  frgrancvvdeqlem4  28178  frgrawopreglem4  28192  frgraregorufr0  28197  2spotiundisj  28207  bnj1373  29151  bnj1489  29177  lshpnel2N  29514  lsatlspsn2  29521  lsatlspsn  29522  lsatspn0  29529  lkrscss  29627  lfl1dim  29650  lfl1dim2N  29651  ldualvs  29666  atpointN  30271  watvalN  30521  trnsetN  30684  dih1dimatlem  31858  dihatexv  31867  dihjat1lem  31957  dihjat1  31958  lcfl7N  32030  lcfl8  32031  lcfl9a  32034  lcfrlem8  32078  lcfrlem9  32079  lcf1o  32080  mapdval2N  32159  mapdval4N  32161  mapdspex  32197  mapdn0  32198  mapdpglem23  32223  mapdpg  32235  mapdindp1  32249  mapdheq  32257  hvmapval  32289  mapdh9a  32319  hdmap1eq  32331  hdmap1cbv  32332  hdmapval  32360  hdmap10  32372  hdmaplkr  32445
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-sn 3807
  Copyright terms: Public domain W3C validator