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

Theorem sneq 4165
Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
sneq (𝐴 = 𝐵 → {𝐴} = {𝐵})

Proof of Theorem sneq
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eqeq2 2632 . . 3 (𝐴 = 𝐵 → (𝑥 = 𝐴𝑥 = 𝐵))
21abbidv 2738 . 2 (𝐴 = 𝐵 → {𝑥𝑥 = 𝐴} = {𝑥𝑥 = 𝐵})
3 df-sn 4156 . 2 {𝐴} = {𝑥𝑥 = 𝐴}
4 df-sn 4156 . 2 {𝐵} = {𝑥𝑥 = 𝐵}
52, 3, 43eqtr4g 2680 1 (𝐴 = 𝐵 → {𝐴} = {𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  {cab 2607  {csn 4155
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-sn 4156
This theorem is referenced by:  sneqi  4166  sneqd  4167  euabsn  4238  absneu  4240  preq1  4245  tpeq3  4256  snssg  4303  issn  4338  sneqrgOLD  4348  sneqbg  4349  opeq1  4377  unisng  4425  propeqop  4940  opthwiener  4946  otiunsndisj  4950  opeliunxp  5141  relop  5242  elimasng  5460  inisegn0  5466  xpdifid  5531  dmsnsnsn  5582  predeq123  5650  suceq  5759  iotajust  5819  fconstg  6059  f1osng  6144  opabiotafun  6226  fvn0ssdmfun  6316  fsng  6369  fsn2g  6370  fnressn  6390  fressnfv  6392  funfvima3  6460  f12dfv  6494  f13dfv  6495  isofrlem  6555  isoselem  6556  snnexOLD  6931  elxp4  7072  elxp5  7073  1stval  7130  2ndval  7131  2ndval2  7146  fo1st  7148  fo2nd  7149  f1stres  7150  f2ndres  7151  mpt2mptsx  7193  dmmpt2ssx  7195  fmpt2x  7196  ovmptss  7218  fparlem3  7239  fparlem4  7240  suppval  7257  suppsnop  7269  ressuppssdif  7276  brtpos2  7318  dftpos4  7331  tpostpos  7332  eceq1  7742  fvdiagfn  7862  mapsncnv  7864  elixpsn  7907  ixpsnf1o  7908  ensn1g  7981  en1  7983  difsnen  8002  xpsneng  8005  xpcomco  8010  xpassen  8014  xpdom2  8015  canth2  8073  phplem3  8101  xpfi  8191  marypha2lem2  8302  cardsn  8755  pm54.43  8786  dfac5lem3  8908  dfac5lem4  8909  kmlem9  8940  kmlem11  8942  kmlem12  8943  ackbij1lem8  9009  r1om  9026  fictb  9027  hsmexlem4  9211  axcc2lem  9218  axcc2  9219  axdc3lem4  9235  fpwwe2cbv  9412  fpwwe2lem3  9415  fpwwecbv  9426  canth4  9429  s3iunsndisj  13657  fsum2dlem  14448  fsumcnv  14451  fsumcom2  14452  fsumcom2OLD  14453  ackbijnn  14504  fprod2dlem  14654  fprodcnv  14657  fprodcom2  14658  fprodcom2OLD  14659  lcmfunsnlem1  15293  lcmfunsnlem2lem1  15294  lcmfunsnlem2lem2  15295  lcmfunsnlem2  15296  lcmfunsn  15300  vdwlem1  15628  vdwlem12  15639  vdwlem13  15640  vdwnn  15645  0ram  15667  ramz2  15671  pwsval  16086  xpsfval  16167  xpsval  16172  symg2bas  17758  symgfixelsi  17795  pmtrfv  17812  pmtrprfval  17847  sylow2a  17974  efgrelexlema  18102  gsum2dlem2  18310  gsum2d2  18313  gsumcom2  18314  dprdcntz  18347  dprddisj  18348  dprd2dlem2  18379  dprd2dlem1  18380  dprd2da  18381  ablfac1eu  18412  ablfaclem3  18426  lssats2  18940  lspsneq0  18952  lbsind  19020  lspsneq  19062  lspdisj2  19067  lspsnsubn0  19080  lspprat  19093  islbs2  19094  lbsextlem4  19101  lbsextg  19102  lpi0  19187  lpi1  19188  psrvsca  19331  evlssca  19462  mpfind  19476  coe1fv  19516  coe1tm  19583  pf1ind  19659  frlmlbs  20076  lindfind  20095  lindsind  20096  lindfrn  20100  submaval  20327  mdetunilem3  20360  mdetunilem4  20361  mdetunilem9  20366  islp  20884  perfi  20899  t1sncld  21070  bwth  21153  dis2ndc  21203  nllyi  21218  dissnlocfin  21272  ptbasfi  21324  txkgen  21395  xkofvcn  21427  xkoinjcn  21430  qtopeu  21459  txswaphmeolem  21547  pt1hmeo  21549  elflim2  21708  cnextfvval  21809  cnextcn  21811  cnextfres1  21812  cnextfres  21813  tsmsxplem1  21896  tsmsxplem2  21897  ucncn  22029  itg11  23398  i1faddlem  23400  i1fmullem  23401  itg1addlem3  23405  itg1mulc  23411  eldv  23602  ply1lpir  23876  areambl  24619  tglngval  25380  nbgrval  26155  nbgr2vtx1edg  26167  nbuhgr2vtx1edgb  26169  nbgr1vtx  26175  nb3grprlem2  26204  uvtxael  26209  uvtxael1  26217  uvtxusgrel  26225  cusgredg  26241  cplgr1v  26247  cplgr3v  26252  usgredgsscusgredg  26276  vtxdgval  26285  1loopgrvd2  26319  wlk1walk  26438  wlkres  26470  wlkp1lem8  26480  usgr2pthlem  26562  crctcshwlkn0lem6  26610  2wspiundisj  26758  1wlkdlem4  26900  eupth2lem3lem3  26990  frcond1  27030  frgr1v  27033  nfrgr2v  27034  frgr3v  27037  1vwmgr  27038  3vfriswmgr  27040  3cyclfrgrrn1  27047  n4cyclfrgr  27053  frgrncvvdeqlem4  27064  frgrwopreglem4  27076  frgrregorufr0  27081  h1de2ctlem  28302  spansn  28306  elspansn  28313  elspansn2  28314  spansneleq  28317  h1datom  28329  spansnj  28394  spansncv  28400  superpos  29101  sumdmdlem2  29166  aciunf1lem  29345  dfcnv2  29360  gsummpt2co  29607  locfinreflem  29731  esum2dlem  29977  sibfima  30223  sibfof  30225  bnj1373  30859  bnj1489  30885  cvmscbv  31001  cvmsdisj  31013  cvmsss2  31017  cvmliftlem15  31041  cvmlift2lem11  31056  cvmlift2lem12  31057  cvmlift2lem13  31058  mvtinf  31213  eldm3  31413  elima4  31434  fvsingle  31722  snelsingles  31724  dfiota3  31725  brapply  31740  funpartlem  31744  altopeq12  31764  ranksng  31969  neibastop3  32052  tailval  32063  filnetlem4  32071  bj-restsnss  32726  bj-restsnss2  32727  f1omptsnlem  32854  f1omptsn  32855  mptsnun  32857  dissneqlem  32858  dissneq  32859  lindsenlbs  33075  poimirlem4  33084  poimirlem25  33105  poimirlem26  33106  poimirlem27  33107  poimirlem31  33111  poimirlem32  33112  heiborlem3  33283  ismrer1  33308  lshpnel2N  33791  lsatlspsn2  33798  lsatlspsn  33799  lsatspn0  33806  lkrscss  33904  lfl1dim  33927  lfl1dim2N  33928  ldualvs  33943  atpointN  34548  watvalN  34798  trnsetN  34962  dih1dimatlem  36137  dihatexv  36146  dihjat1lem  36236  dihjat1  36237  lcfl7N  36309  lcfl8  36310  lcfl9a  36313  lcfrlem8  36357  lcfrlem9  36358  lcf1o  36359  mapdval2N  36438  mapdval4N  36440  mapdspex  36476  mapdn0  36477  mapdpglem23  36502  mapdpg  36514  mapdindp1  36528  mapdheq  36536  hvmapval  36568  mapdh9a  36598  hdmap1eq  36610  hdmap1cbv  36611  hdmapval  36639  hdmap10  36651  hdmaplkr  36724  mzpclval  36807  mzpcl1  36811  wopprc  37116  dnnumch3lem  37135  aomclem8  37150  mendvsca  37281  cytpval  37307  k0004lem3  37968  dvconstbi  38054  wessf1ornlem  38880  dvmptfprodlem  39496  fourierdlem32  39693  fourierdlem33  39694  fourierdlem48  39708  fzopredsuc  40660  elsprel  41043  irinitoringc  41387  opeliun2xp  41429  dmmpt2ssx2  41433  lindslinindsimp2  41570  ldepspr  41580  ldepsnlinc  41615
  Copyright terms: Public domain W3C validator