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

Theorem sneq 4135
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 2621 . . 3 (𝐴 = 𝐵 → (𝑥 = 𝐴𝑥 = 𝐵))
21abbidv 2728 . 2 (𝐴 = 𝐵 → {𝑥𝑥 = 𝐴} = {𝑥𝑥 = 𝐵})
3 df-sn 4126 . 2 {𝐴} = {𝑥𝑥 = 𝐴}
4 df-sn 4126 . 2 {𝐵} = {𝑥𝑥 = 𝐵}
52, 3, 43eqtr4g 2669 1 (𝐴 = 𝐵 → {𝐴} = {𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  {cab 2596  {csn 4125
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-sn 4126
This theorem is referenced by:  sneqi  4136  sneqd  4137  euabsn  4205  absneu  4207  preq1  4212  tpeq3  4223  snssg  4268  issn  4303  sneqrgOLD  4313  sneqbg  4314  opeq1  4340  unisng  4388  propeqop  4895  opthwiener  4901  otiunsndisj  4905  opeliunxp  5093  relop  5194  elimasng  5410  inisegn0  5416  xpdifid  5481  dmsnsnsn  5531  predeq123  5598  suceq  5707  iotajust  5767  fconstg  6005  f1osng  6089  opabiotafun  6169  fvn0ssdmfun  6258  fsng  6310  fsn2g  6311  fnressn  6330  fressnfv  6332  funfvima3  6399  f12dfv  6429  f13dfv  6430  isofrlem  6490  isoselem  6491  snnex  6862  elxp4  7003  elxp5  7004  1stval  7061  2ndval  7062  2ndval2  7077  fo1st  7079  fo2nd  7080  f1stres  7081  f2ndres  7082  mpt2mptsx  7122  dmmpt2ssx  7124  fmpt2x  7125  ovmptss  7145  fparlem3  7166  fparlem4  7167  suppval  7184  suppsnop  7196  ressuppssdif  7203  brtpos2  7245  dftpos4  7258  tpostpos  7259  eceq1  7669  fvdiagfn  7788  mapsncnv  7790  elixpsn  7833  ixpsnf1o  7834  ensn1g  7907  en1  7909  difsnen  7927  xpsneng  7930  xpcomco  7935  xpassen  7939  xpdom2  7940  canth2  7998  phplem3  8026  xpfi  8116  marypha2lem2  8225  cardsn  8678  pm54.43  8709  dfac5lem3  8831  dfac5lem4  8832  kmlem9  8863  kmlem11  8865  kmlem12  8866  ackbij1lem8  8932  r1om  8949  fictb  8950  hsmexlem4  9134  axcc2lem  9141  axcc2  9142  axdc3lem4  9158  fpwwe2cbv  9331  fpwwe2lem3  9334  fpwwecbv  9345  canth4  9348  s3iunsndisj  13555  fsum2dlem  14343  fsumcnv  14346  fsumcom2  14347  fsumcom2OLD  14348  ackbijnn  14399  fprod2dlem  14549  fprodcnv  14552  fprodcom2  14553  fprodcom2OLD  14554  lcmfunsnlem1  15188  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  lcmfunsnlem2  15191  lcmfunsn  15195  vdwlem1  15523  vdwlem12  15534  vdwlem13  15535  vdwnn  15540  0ram  15562  ramz2  15566  pwsval  15969  xpsfval  16050  xpsval  16055  symg2bas  17641  symgfixelsi  17678  pmtrfv  17695  pmtrprfval  17730  sylow2a  17857  efgrelexlema  17985  gsum2dlem2  18193  gsum2d2  18196  gsumcom2  18197  dprdcntz  18230  dprddisj  18231  dprd2dlem2  18262  dprd2dlem1  18263  dprd2da  18264  ablfac1eu  18295  ablfaclem3  18309  lssats2  18821  lspsneq0  18833  lbsind  18901  lspsneq  18943  lspdisj2  18948  lspsnsubn0  18961  lspprat  18974  islbs2  18975  lbsextlem4  18982  lbsextg  18983  lpi0  19068  lpi1  19069  psrvsca  19212  evlssca  19343  mpfind  19357  coe1fv  19397  coe1tm  19464  pf1ind  19540  frlmlbs  19955  lindfind  19974  lindsind  19975  lindfrn  19979  submaval  20206  mdetunilem3  20239  mdetunilem4  20240  mdetunilem9  20245  islp  20754  perfi  20769  t1sncld  20940  bwth  21023  dis2ndc  21073  nllyi  21088  dissnlocfin  21142  ptbasfi  21194  txkgen  21265  xkofvcn  21297  xkoinjcn  21300  qtopeu  21329  txswaphmeolem  21417  pt1hmeo  21419  elflim2  21578  cnextfvval  21679  cnextcn  21681  cnextfres1  21682  cnextfres  21683  tsmsxplem1  21766  tsmsxplem2  21767  ucncn  21899  itg11  23264  i1faddlem  23266  i1fmullem  23267  itg1addlem3  23271  itg1mulc  23277  eldv  23468  ply1lpir  23742  areambl  24485  tglngval  25246  nbgraopALT  25953  nb3graprlem2  25981  cusgrarn  25988  cusgra1v  25990  cusgra2v  25991  cusgra3v  25993  cusgrares  26001  usgrasscusgra  26011  sizeusglecusglem1  26012  uvtxel  26017  cusgrauvtxb  26024  vdgrval  26423  frgraunss  26522  frgra1v  26525  frgra2v  26526  frgra3v  26529  1vwmgra  26530  3vfriswmgra  26532  3cyclfrgrarn1  26539  n4cyclfrgra  26545  frgrancvvdeqlem4  26560  frgrawopreglem4  26574  frgraregorufr0  26579  2spotiundisj  26589  h1de2ctlem  27798  spansn  27802  elspansn  27809  elspansn2  27810  spansneleq  27813  h1datom  27825  spansnj  27890  spansncv  27896  superpos  28597  sumdmdlem2  28662  aciunf1lem  28844  dfcnv2  28859  gsummpt2co  29111  locfinreflem  29235  esum2dlem  29481  sibfima  29727  sibfof  29729  bnj1373  30352  bnj1489  30378  cvmscbv  30494  cvmsdisj  30506  cvmsss2  30510  cvmliftlem15  30534  cvmlift2lem11  30549  cvmlift2lem12  30550  cvmlift2lem13  30551  mvtinf  30706  eldm3  30905  elima4  30924  fvsingle  31197  snelsingles  31199  dfiota3  31200  brapply  31215  funpartlem  31219  altopeq12  31239  ranksng  31444  neibastop3  31527  tailval  31538  filnetlem4  31546  bj-restsnss  32217  bj-restsnss2  32218  f1omptsnlem  32359  f1omptsn  32360  mptsnun  32362  dissneqlem  32363  dissneq  32364  lindsenlbs  32574  poimirlem4  32583  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem31  32610  poimirlem32  32611  heiborlem3  32782  ismrer1  32807  lshpnel2N  33290  lsatlspsn2  33297  lsatlspsn  33298  lsatspn0  33305  lkrscss  33403  lfl1dim  33426  lfl1dim2N  33427  ldualvs  33442  atpointN  34047  watvalN  34297  trnsetN  34461  dih1dimatlem  35636  dihatexv  35645  dihjat1lem  35735  dihjat1  35736  lcfl7N  35808  lcfl8  35809  lcfl9a  35812  lcfrlem8  35856  lcfrlem9  35857  lcf1o  35858  mapdval2N  35937  mapdval4N  35939  mapdspex  35975  mapdn0  35976  mapdpglem23  36001  mapdpg  36013  mapdindp1  36027  mapdheq  36035  hvmapval  36067  mapdh9a  36097  hdmap1eq  36109  hdmap1cbv  36110  hdmapval  36138  hdmap10  36150  hdmaplkr  36223  mzpclval  36306  mzpcl1  36310  wopprc  36615  dnnumch3lem  36634  aomclem8  36649  mendvsca  36780  cytpval  36806  k0004lem3  37467  dvconstbi  37555  wessf1ornlem  38366  dvmptfprodlem  38834  fourierdlem32  39032  fourierdlem33  39033  fourierdlem48  39047  fzopredsuc  39946  nbgrval  40560  nbgr2vtx1edg  40572  nbuhgr2vtx1edgb  40574  nbgr1vtx  40580  nb3grprlem2  40609  uvtxael  40614  uvtxael1  40622  uvtxusgrel  40630  cusgredg  40646  cplgr1v  40652  cplgr3v  40657  usgredgsscusgredg  40675  vtxdgval  40684  1loopgrvd2  40718  1wlk1walk  40843  1wlkres  40879  1wlkp1lem8  40889  usgr2pthlem  40969  crctcsh1wlkn0lem6  41018  2wspiundisj  41166  11wlkdlem4  41307  eupth2lem3lem3  41398  frcond1  41438  frgr1v  41441  nfrgr2v  41442  frgr3v  41445  1vwmgr  41446  3vfriswmgr  41448  3cyclfrgrrn1  41455  n4cyclfrgr  41461  frgrncvvdeqlem4  41472  frgrwopreglem4  41484  frgrregorufr0  41489  irinitoringc  41861  opeliun2xp  41904  dmmpt2ssx2  41908  lindslinindsimp2  42046  ldepspr  42056  ldepsnlinc  42091
  Copyright terms: Public domain W3C validator