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

Theorem sneq 3653
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 } )
Dummy variable  x is distinct from all other variables.

Proof of Theorem sneq
StepHypRef Expression
1 eqeq2 2294 . . 3  |-  ( A  =  B  ->  (
x  =  A  <->  x  =  B ) )
21abbidv 2399 . 2  |-  ( A  =  B  ->  { x  |  x  =  A }  =  { x  |  x  =  B } )
3 df-sn 3648 . 2  |-  { A }  =  { x  |  x  =  A }
4 df-sn 3648 . 2  |-  { B }  =  { x  |  x  =  B }
52, 3, 43eqtr4g 2342 1  |-  ( A  =  B  ->  { A }  =  { B } )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1624   {cab 2271   {csn 3642
This theorem is referenced by:  sneqi  3654  sneqd  3655  euabsn  3701  absneu  3703  preq1  3708  tpeq3  3719  snssg  3756  sneqrg  3784  sneqbg  3785  opeq1  3798  unisng  3846  opthwiener  4268  suceq  4457  snnex  4524  opeliunxp  4740  relop  4834  elimasng  5039  dmsnsnsn  5150  elxp4  5159  elxp5  5160  fconstg  5394  f1osng  5480  fveq2  5486  fsng  5659  fnressn  5667  fressnfv  5669  funfvima3  5717  isofrlem  5799  isoselem  5800  1stval  6086  2ndval  6087  2ndval2  6100  fo1st  6101  fo2nd  6102  f1stres  6103  f2ndres  6104  mpt2mptsx  6149  dmmpt2ssx  6151  fmpt2x  6152  ovmptss  6162  fparlem3  6182  fparlem4  6183  brtpos2  6202  dftpos4  6215  tpostpos  6216  iotajust  6252  opabiotafun  6285  eceq1  6692  fvdiagfn  6808  mapsncnv  6810  elixpsn  6851  ixpsnf1o  6852  ensn1g  6922  en1  6924  difsnen  6940  xpsneng  6943  xpcomco  6948  xpassen  6952  xpdom2  6953  canth2  7010  phplem3  7038  xpfi  7124  marypha2lem2  7185  cardsn  7598  pm54.43  7629  dfac5lem3  7748  dfac5lem4  7749  kmlem9  7780  kmlem11  7782  kmlem12  7783  ackbij1lem8  7849  r1om  7866  fictb  7867  hsmexlem4  8051  axcc2lem  8058  axcc2  8059  axdc3lem4  8075  fpwwe2cbv  8248  fpwwe2lem3  8251  fpwwecbv  8262  canth4  8265  fsum2dlem  12228  fsumcnv  12231  fsumcom2  12232  ackbijnn  12281  xpnnenOLD  12483  vdwlem1  13023  vdwlem12  13034  vdwlem13  13035  vdwnn  13040  0ram  13062  ramz2  13066  pwsval  13380  xpsfval  13464  xpsval  13469  sylow2a  14925  efgrelexlema  15053  gsum2d  15218  gsum2d2  15220  gsumcom2  15221  dprdcntz  15238  dprddisj  15239  dprd2dlem2  15270  dprd2dlem1  15271  dprd2da  15272  ablfac1eu  15303  ablfaclem3  15317  lssats2  15752  lspsneq0  15764  lbsind  15828  lspsneq  15870  lspdisj2  15875  lspsnsubn0  15888  lspprat  15901  islbs2  15902  lbsextlem4  15909  lbsextg  15910  lpi0  15994  lpi1  15995  psrvsca  16131  coe1fv  16282  coe1tm  16344  islp  16867  perfi  16881  t1sncld  17049  dis2ndc  17181  nllyi  17196  ptbasfi  17271  txkgen  17341  xkofvcn  17373  xkoinjcn  17376  qtopeu  17402  txswaphmeolem  17490  pt1hmeo  17492  elflim2  17654  tsmsxplem1  17830  tsmsxplem2  17831  itg11  19041  i1faddlem  19043  i1fmullem  19044  itg1addlem3  19048  itg1mulc  19054  eldv  19243  evlssca  19401  mpfind  19423  pf1ind  19433  ply1lpir  19559  areambl  20248  gxval  20918  h1de2ctlem  22127  spansn  22131  elspansn  22138  elspansn2  22139  spansneleq  22142  h1datom  22154  spansnj  22219  spansncv  22225  superpos  22927  sumdmdlem2  22992  cvmscbv  23194  cvmsdisj  23206  cvmsss2  23210  cvmliftlem15  23234  cvmlift2lem11  23249  cvmlift2lem12  23250  cvmlift2lem13  23251  vdgrval  23295  predeq3  23573  fvsingle  23867  snelsingles  23869  dfiota3  23870  brapply  23885  funpartfv  23891  altopeq12  23904  ranksng  24205  fatesg  24355  snelpwg  24490  cbicp  24566  valcurfn1  24604  osneisi  24931  islimrs  24980  isder  25107  valtar  25283  lineval222  25479  lineval3a  25483  sgplpte21  25532  sgplpte22  25538  isray2  25553  isray  25554  neibastop3  25711  tailval  25722  filnetlem4  25730  heiborlem3  25937  ismrer1  25962  mzpclval  26203  mzpcl1  26207  wopprc  26523  inisegn0  26540  dnnumch3lem  26543  aomclem8  26559  frlmlbs  26649  mapfien2  26658  lindfind  26686  lindsind  26687  lindfrn  26691  pmtrfv  26795  mendvsca  26899  cytpval  26928  dvconstbi  26951  bnj1373  28328  bnj1489  28354  lshpnel2N  28443  lsatlspsn2  28450  lsatlspsn  28451  lsatspn0  28458  lkrscss  28556  lfl1dim  28579  lfl1dim2N  28580  ldualvs  28595  atpointN  29200  watvalN  29450  trnsetN  29613  dih1dimatlem  30787  dihatexv  30796  dihjat1lem  30886  dihjat1  30887  lcfl7N  30959  lcfl8  30960  lcfl9a  30963  lcfrlem8  31007  lcfrlem9  31008  lcf1o  31009  mapdval2N  31088  mapdval4N  31090  mapdspex  31126  mapdn0  31127  mapdpglem23  31152  mapdpg  31164  mapdindp1  31178  mapdheq  31186  hvmapval  31218  mapdh9a  31248  hdmap1eq  31260  hdmap1cbv  31261  hdmapval  31289  hdmap10  31301  hdmaplkr  31374
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-sn 3648
  Copyright terms: Public domain W3C validator