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

Theorem sneq 4329
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 2769 . . 3 (𝐴 = 𝐵 → (𝑥 = 𝐴𝑥 = 𝐵))
21abbidv 2877 . 2 (𝐴 = 𝐵 → {𝑥𝑥 = 𝐴} = {𝑥𝑥 = 𝐵})
3 df-sn 4320 . 2 {𝐴} = {𝑥𝑥 = 𝐴}
4 df-sn 4320 . 2 {𝐵} = {𝑥𝑥 = 𝐵}
52, 3, 43eqtr4g 2817 1 (𝐴 = 𝐵 → {𝐴} = {𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1630  {cab 2744  {csn 4319
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-sn 4320
This theorem is referenced by:  sneqi  4330  sneqd  4331  euabsn  4403  absneu  4405  preq1  4410  tpeq3  4421  snssgOLD  4459  issn  4506  sneqrgOLD  4516  sneqbg  4517  opeq1  4551  unisng  4602  propeqop  5116  opthwiener  5122  otiunsndisj  5128  opeliunxp  5325  relop  5426  elimasng  5647  inisegn0  5653  xpdifid  5718  dmsnsnsn  5770  predeq123  5840  suceq  5949  iotajust  6009  fconstg  6251  f1osng  6336  opabiotafun  6419  fvn0ssdmfun  6511  fsng  6565  fsn2g  6566  fnressn  6586  fressnfv  6588  funfvima3  6656  f12dfv  6690  f13dfv  6691  isofrlem  6751  isoselem  6752  snnexOLD  7130  elxp4  7273  elxp5  7274  1stval  7333  2ndval  7334  2ndval2  7349  fo1st  7351  fo2nd  7352  f1stres  7355  f2ndres  7356  mpt2mptsx  7399  dmmpt2ssx  7401  fmpt2x  7402  ovmptss  7424  fparlem3  7445  fparlem4  7446  suppval  7463  suppsnop  7475  ressuppssdif  7482  brtpos2  7525  dftpos4  7538  tpostpos  7539  eceq1  7947  fvdiagfn  8066  mapsncnv  8068  elixpsn  8111  ixpsnf1o  8112  ensn1g  8184  en1  8186  difsnen  8205  xpsneng  8208  xpcomco  8213  xpassen  8217  xpdom2  8218  canth2  8276  phplem3  8304  xpfi  8394  marypha2lem2  8505  cardsn  8983  pm54.43  9014  dfac5lem3  9136  dfac5lem4  9137  kmlem9  9170  kmlem11  9172  kmlem12  9173  ackbij1lem8  9239  r1om  9256  fictb  9257  hsmexlem4  9441  axcc2lem  9448  axcc2  9449  axdc3lem4  9465  fpwwe2cbv  9642  fpwwe2lem3  9645  fpwwecbv  9656  canth4  9659  s3iunsndisj  13906  fsum2dlem  14698  fsumcnv  14701  fsumcom2  14702  fsumcom2OLD  14703  ackbijnn  14757  fprod2dlem  14907  fprodcnv  14910  fprodcom2  14911  fprodcom2OLD  14912  lcmfunsnlem1  15550  lcmfunsnlem2lem1  15551  lcmfunsnlem2lem2  15552  lcmfunsnlem2  15553  lcmfunsn  15557  vdwlem1  15885  vdwlem12  15896  vdwlem13  15897  vdwnn  15902  0ram  15924  ramz2  15928  pwsval  16346  xpsfval  16427  xpsval  16432  symg2bas  18016  symgfixelsi  18053  pmtrfv  18070  pmtrprfval  18105  sylow2a  18232  efgrelexlema  18360  gsum2dlem2  18568  gsum2d2  18571  gsumcom2  18572  dprdcntz  18605  dprddisj  18606  dprd2dlem2  18637  dprd2dlem1  18638  dprd2da  18639  ablfac1eu  18670  ablfaclem3  18684  lssats2  19200  lspsneq0  19212  lbsind  19280  lspsneq  19322  lspdisj2  19327  lspsnsubn0  19340  lspprat  19353  islbs2  19354  lbsextlem4  19361  lbsextg  19362  lpi0  19447  lpi1  19448  psrvsca  19591  evlssca  19722  mpfind  19736  coe1fv  19776  coe1tm  19843  pf1ind  19919  frlmlbs  20336  lindfind  20355  lindsind  20356  lindfrn  20360  submaval  20587  mdetunilem3  20620  mdetunilem4  20621  mdetunilem9  20626  islp  21144  perfi  21159  t1sncld  21330  bwth  21413  dis2ndc  21463  nllyi  21478  dissnlocfin  21532  ptbasfi  21584  txkgen  21655  xkofvcn  21687  xkoinjcn  21690  qtopeu  21719  txswaphmeolem  21807  pt1hmeo  21809  elflim2  21967  cnextfvval  22068  cnextcn  22070  cnextfres1  22071  cnextfres  22072  tsmsxplem1  22155  tsmsxplem2  22156  ucncn  22288  itg11  23655  i1faddlem  23657  i1fmullem  23658  itg1addlem3  23662  itg1mulc  23668  eldv  23859  ply1lpir  24135  areambl  24882  tglngval  25643  edglnl  26235  nbgrval  26426  nbgr2vtx1edg  26443  nbuhgr2vtx1edgb  26445  nbgr1vtx  26451  nb3grprlem2  26479  uvtxel  26487  uvtxaelOLD  26488  uvtxel1  26497  uvtxael1OLD  26499  uvtxusgrel  26506  cusgredg  26528  cplgr1v  26534  cplgr3v  26539  usgredgsscusgredg  26563  vtxdgval  26572  1loopgrvd2  26607  wlk1walk  26743  wlkres  26775  wlkp1lem8  26785  usgr2pthlem  26867  crctcshwlkn0lem6  26916  2wspiundisj  27083  clwwlknon1  27243  1wlkdlem4  27290  eupth2lem3lem3  27380  frcond1  27418  frgr1v  27423  nfrgr2v  27424  frgr3v  27427  1vwmgr  27428  3vfriswmgr  27430  3cyclfrgrrn1  27437  n4cyclfrgr  27443  frgrwopreglem4a  27462  h1de2ctlem  28721  spansn  28725  elspansn  28732  elspansn2  28733  spansneleq  28736  h1datom  28748  spansnj  28813  spansncv  28819  superpos  29520  sumdmdlem2  29585  aciunf1lem  29769  dfcnv2  29783  gsummpt2co  30087  locfinreflem  30214  esum2dlem  30461  sibfima  30707  sibfof  30709  bnj1373  31403  bnj1489  31429  cvmscbv  31545  cvmsdisj  31557  cvmsss2  31561  cvmliftlem15  31585  cvmlift2lem11  31600  cvmlift2lem12  31601  cvmlift2lem13  31602  mvtinf  31757  eldm3  31956  elima4  31982  conway  32214  scutval  32215  scutcut  32216  scutbday  32217  scutun12  32221  scutbdaybnd  32225  scutbdaylt  32226  fvsingle  32331  snelsingles  32333  dfiota3  32334  brapply  32349  funpartlem  32353  altopeq12  32373  ranksng  32578  neibastop3  32661  tailval  32672  filnetlem4  32680  bj-restsnss  33340  bj-restsnss2  33341  f1omptsnlem  33492  f1omptsn  33493  mptsnun  33495  dissneqlem  33496  dissneq  33497  lindsenlbs  33715  poimirlem4  33724  poimirlem25  33745  poimirlem26  33746  poimirlem27  33747  poimirlem31  33751  poimirlem32  33752  heiborlem3  33923  ismrer1  33948  lshpnel2N  34773  lsatlspsn2  34780  lsatlspsn  34781  lsatspn0  34788  lkrscss  34886  lfl1dim  34909  lfl1dim2N  34910  ldualvs  34925  atpointN  35530  watvalN  35780  trnsetN  35944  dih1dimatlem  37118  dihatexv  37127  dihjat1lem  37217  dihjat1  37218  lcfl7N  37290  lcfl8  37291  lcfl9a  37294  lcfrlem8  37338  lcfrlem9  37339  lcf1o  37340  mapdval2N  37419  mapdval4N  37421  mapdspex  37457  mapdn0  37458  mapdpglem23  37483  mapdpg  37495  mapdindp1  37509  mapdheq  37517  hvmapval  37549  mapdh9a  37579  hdmap1eq  37591  hdmap1cbv  37592  hdmapval  37620  hdmap10  37632  hdmaplkr  37705  mzpclval  37788  mzpcl1  37792  wopprc  38097  dnnumch3lem  38116  aomclem8  38131  mendvsca  38261  cytpval  38287  k0004lem3  38947  dvconstbi  39033  wessf1ornlem  39868  dvmptfprodlem  40660  fourierdlem32  40857  fourierdlem33  40858  fourierdlem48  40872  fzopredsuc  41841  elsprel  42233  irinitoringc  42577  opeliun2xp  42619  dmmpt2ssx2  42623  lindslinindsimp2  42760  ldepspr  42770  ldepsnlinc  42805
  Copyright terms: Public domain W3C validator