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

Theorem sneq 3849
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 2451 . . 3  |-  ( A  =  B  ->  (
x  =  A  <->  x  =  B ) )
21abbidv 2556 . 2  |-  ( A  =  B  ->  { x  |  x  =  A }  =  { x  |  x  =  B } )
3 df-sn 3844 . 2  |-  { A }  =  { x  |  x  =  A }
4 df-sn 3844 . 2  |-  { B }  =  { x  |  x  =  B }
52, 3, 43eqtr4g 2499 1  |-  ( A  =  B  ->  { A }  =  { B } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   {cab 2428   {csn 3838
This theorem is referenced by:  sneqi  3850  sneqd  3851  euabsn  3900  absneu  3902  preq1  3907  tpeq3  3918  snssg  3956  sneqrg  3992  sneqbg  3993  opeq1  4008  unisng  4056  opthwiener  4487  suceq  4675  snnex  4742  opeliunxp  4958  relop  5052  elimasng  5259  dmsnsnsn  5377  elxp4  5386  elxp5  5387  iotajust  5446  fconstg  5659  f1osng  5745  fsng  5936  fnressn  5947  fressnfv  5949  funfvima3  6004  isofrlem  6089  isoselem  6090  1stval  6380  2ndval  6381  2ndval2  6394  fo1st  6395  fo2nd  6396  f1stres  6397  f2ndres  6398  mpt2mptsx  6443  dmmpt2ssx  6445  fmpt2x  6446  ovmptss  6457  fparlem3  6477  fparlem4  6478  brtpos2  6514  dftpos4  6527  tpostpos  6528  opabiotafun  6565  eceq1  6970  fvdiagfn  7087  mapsncnv  7089  elixpsn  7130  ixpsnf1o  7131  ensn1g  7201  en1  7203  difsnen  7219  xpsneng  7222  xpcomco  7227  xpassen  7231  xpdom2  7232  canth2  7289  phplem3  7317  xpfi  7407  marypha2lem2  7470  cardsn  7887  pm54.43  7918  dfac5lem3  8037  dfac5lem4  8038  kmlem9  8069  kmlem11  8071  kmlem12  8072  ackbij1lem8  8138  r1om  8155  fictb  8156  hsmexlem4  8340  axcc2lem  8347  axcc2  8348  axdc3lem4  8364  fpwwe2cbv  8536  fpwwe2lem3  8539  fpwwecbv  8550  canth4  8553  fsum2dlem  12585  fsumcnv  12588  fsumcom2  12589  ackbijnn  12638  xpnnenOLD  12840  vdwlem1  13380  vdwlem12  13391  vdwlem13  13392  vdwnn  13397  0ram  13419  ramz2  13423  pwsval  13739  xpsfval  13823  xpsval  13828  sylow2a  15284  efgrelexlema  15412  gsum2d  15577  gsum2d2  15579  gsumcom2  15580  dprdcntz  15597  dprddisj  15598  dprd2dlem2  15629  dprd2dlem1  15630  dprd2da  15631  ablfac1eu  15662  ablfaclem3  15676  lssats2  16107  lspsneq0  16119  lbsind  16183  lspsneq  16225  lspdisj2  16230  lspsnsubn0  16243  lspprat  16256  islbs2  16257  lbsextlem4  16264  lbsextg  16265  lpi0  16349  lpi1  16350  psrvsca  16486  coe1fv  16635  coe1tm  16696  islp  17235  perfi  17250  t1sncld  17421  dis2ndc  17554  nllyi  17569  ptbasfi  17644  txkgen  17715  xkofvcn  17747  xkoinjcn  17750  qtopeu  17779  txswaphmeolem  17867  pt1hmeo  17869  elflim2  18027  cnextfvval  18127  cnextcn  18129  cnextfres  18130  tsmsxplem1  18213  tsmsxplem2  18214  ucncn  18346  itg11  19612  i1faddlem  19614  i1fmullem  19615  itg1addlem3  19619  itg1mulc  19625  eldv  19816  evlssca  19974  mpfind  19996  pf1ind  20006  ply1lpir  20132  areambl  20828  nb3graprlem2  21492  cusgrarn  21499  cusgra1v  21501  cusgra2v  21502  cusgra3v  21504  cusgrares  21512  usgrasscusgra  21523  sizeusglecusglem1  21524  uvtxel  21529  cusgrauvtxb  21536  vdgrval  21698  gxval  21877  h1de2ctlem  23088  spansn  23092  elspansn  23099  elspansn2  23100  spansneleq  23103  h1datom  23115  spansnj  23180  spansncv  23186  superpos  23888  sumdmdlem2  23953  sibfima  24684  sibfof  24685  cvmscbv  24976  cvmsdisj  24988  cvmsss2  24992  cvmliftlem15  25016  cvmlift2lem11  25031  cvmlift2lem12  25032  cvmlift2lem13  25033  fprod2dlem  25335  fprodcnv  25338  fprodcom2  25339  eldm3  25416  elima4  25435  predeq123  25471  fvsingle  25796  snelsingles  25798  dfiota3  25799  brapply  25814  funpartlem  25818  altopeq12  25838  ranksng  26139  neibastop3  26429  tailval  26440  filnetlem4  26448  heiborlem3  26560  ismrer1  26585  mzpclval  26820  mzpcl1  26824  wopprc  27139  inisegn0  27156  dnnumch3lem  27159  aomclem8  27174  frlmlbs  27264  mapfien2  27273  lindfind  27301  lindsind  27302  lindfrn  27306  pmtrfv  27410  mendvsca  27514  cytpval  27543  dvconstbi  27566  otiunsndisj  28105  f12dfv  28122  f13dfv  28123  usgra2pthlem1  28372  frgraunss  28483  frgra1v  28486  frgra2v  28487  frgra3v  28490  1vwmgra  28491  3vfriswmgra  28493  3cyclfrgrarn1  28500  n4cyclfrgra  28506  frgrancvvdeqlem4  28520  frgrawopreglem4  28534  frgraregorufr0  28539  2spotiundisj  28549  bnj1373  29497  bnj1489  29523  lshpnel2N  29881  lsatlspsn2  29888  lsatlspsn  29889  lsatspn0  29896  lkrscss  29994  lfl1dim  30017  lfl1dim2N  30018  ldualvs  30033  atpointN  30638  watvalN  30888  trnsetN  31051  dih1dimatlem  32225  dihatexv  32234  dihjat1lem  32324  dihjat1  32325  lcfl7N  32397  lcfl8  32398  lcfl9a  32401  lcfrlem8  32445  lcfrlem9  32446  lcf1o  32447  mapdval2N  32526  mapdval4N  32528  mapdspex  32564  mapdn0  32565  mapdpglem23  32590  mapdpg  32602  mapdindp1  32616  mapdheq  32624  hvmapval  32656  mapdh9a  32686  hdmap1eq  32698  hdmap1cbv  32699  hdmapval  32727  hdmap10  32739  hdmaplkr  32812
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-sn 3844
  Copyright terms: Public domain W3C validator