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

Theorem sneq 4380
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 2817 . . 3 (𝐴 = 𝐵 → (𝑥 = 𝐴𝑥 = 𝐵))
21abbidv 2925 . 2 (𝐴 = 𝐵 → {𝑥𝑥 = 𝐴} = {𝑥𝑥 = 𝐵})
3 df-sn 4371 . 2 {𝐴} = {𝑥𝑥 = 𝐴}
4 df-sn 4371 . 2 {𝐵} = {𝑥𝑥 = 𝐵}
52, 3, 43eqtr4g 2865 1 (𝐴 = 𝐵 → {𝐴} = {𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  {cab 2792  {csn 4370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-sn 4371
This theorem is referenced by:  sneqi  4381  sneqd  4382  euabsn  4452  absneu  4454  preq1  4459  tpeq3  4470  snssgOLD  4507  issn  4551  mosneq  4561  sneqbg  4562  opeq1  4595  unisngOLD  4648  propeqop  5162  opthwiener  5169  otiunsndisj  5175  opeliunxp  5370  relop  5474  elimasng  5701  inisegn0  5707  xpdifid  5773  dmsnsnsn  5825  predeq123  5894  suceq  6002  iotajust  6059  fconstg  6303  f1osng  6389  opabiotafun  6476  fvn0ssdmfun  6568  fsng  6623  fsn2g  6624  fnressn  6645  fressnfv  6647  funfvima3  6716  f12dfv  6749  f13dfv  6750  isofrlem  6810  isoselem  6811  snnexOLD  7193  elxp4  7336  elxp5  7337  1stval  7396  2ndval  7397  2ndval2  7412  fo1st  7414  fo2nd  7415  f1stres  7418  f2ndres  7419  mpt2mptsx  7462  dmmpt2ssx  7464  fmpt2x  7465  ovmptss  7488  fparlem3  7509  fparlem4  7510  suppval  7527  suppsnop  7539  ressuppssdif  7546  brtpos2  7589  dftpos4  7602  tpostpos  7603  eceq1  8013  fvdiagfn  8135  mapsncnv  8137  elixpsn  8180  ixpsnf1o  8181  ensn1g  8253  en1  8255  difsnen  8277  xpsneng  8280  xpcomco  8285  xpassen  8289  xpdom2  8290  canth2  8348  phplem3  8376  xpfi  8466  marypha2lem2  8577  cardsn  9074  pm54.43  9105  dfac5lem3  9227  dfac5lem4  9228  kmlem9  9261  kmlem11  9263  kmlem12  9264  ackbij1lem8  9330  r1om  9347  fictb  9348  hsmexlem4  9532  axcc2lem  9539  axcc2  9540  axdc3lem4  9556  fpwwe2cbv  9733  fpwwe2lem3  9736  fpwwecbv  9747  canth4  9750  s3iunsndisj  13928  fsum2dlem  14720  fsumcnv  14723  fsumcom2  14724  ackbijnn  14778  fprod2dlem  14927  fprodcnv  14930  fprodcom2  14931  lcmfunsnlem1  15565  lcmfunsnlem2lem1  15566  lcmfunsnlem2lem2  15567  lcmfunsnlem2  15568  lcmfunsn  15572  vdwlem1  15898  vdwlem12  15909  vdwlem13  15910  vdwnn  15915  0ram  15937  ramz2  15941  pwsval  16347  xpsfval  16428  xpsval  16433  symg2bas  18015  symgfixelsi  18052  pmtrfv  18069  pmtrprfval  18104  sylow2a  18231  efgrelexlema  18359  gsum2dlem2  18567  gsum2d2  18570  gsumcom2  18571  dprdcntz  18605  dprddisj  18606  dprd2dlem2  18637  dprd2dlem1  18638  dprd2da  18639  ablfac1eu  18670  ablfaclem3  18684  lssats2  19203  lspsneq0  19215  lbsind  19283  lspsneq  19325  lspdisj2  19330  lspsnsubn0  19344  lspprat  19358  islbs2  19359  lbsextlem4  19366  lbsextg  19367  lpi0  19452  lpi1  19453  psrvsca  19596  evlssca  19726  mpfind  19740  coe1fv  19780  coe1tm  19847  pf1ind  19923  frlmlbs  20342  lindfind  20361  lindsind  20362  lindfrn  20366  submaval  20594  mdetunilem3  20627  mdetunilem4  20628  mdetunilem9  20633  islp  21154  perfi  21169  t1sncld  21340  bwth  21423  dis2ndc  21473  nllyi  21488  dissnlocfin  21542  ptbasfi  21594  txkgen  21665  xkofvcn  21697  xkoinjcn  21700  qtopeu  21729  txswaphmeolem  21817  pt1hmeo  21819  elflim2  21977  cnextfvval  22078  cnextcn  22080  cnextfres1  22081  cnextfres  22082  tsmsxplem1  22165  tsmsxplem2  22166  ucncn  22298  itg11  23668  i1faddlem  23670  i1fmullem  23671  itg1addlem3  23675  itg1mulc  23681  eldv  23872  ply1lpir  24148  areambl  24895  tglngval  25656  edglnl  26249  nbgrval  26441  nbgr2vtx1edg  26458  nbuhgr2vtx1edgb  26460  nbgr1vtx  26466  nb3grprlem2  26495  uvtxel  26503  uvtxaelOLD  26504  uvtxel1  26513  uvtxael1OLD  26515  uvtxusgrel  26522  cusgredg  26544  cplgr1v  26550  cplgr3v  26555  usgredgsscusgredg  26579  vtxdgval  26588  1loopgrvd2  26623  wlk1walk  26759  wlkres  26791  wlkp1lem8  26801  usgr2pthlem  26883  crctcshwlkn0lem6  26932  2wspiundisj  27101  clwwlknon1  27261  1wlkdlem4  27309  eupth2lem3lem3  27399  frcond1  27437  frgr1v  27442  nfrgr2v  27443  frgr3v  27446  1vwmgr  27447  3vfriswmgr  27449  3cyclfrgrrn1  27456  n4cyclfrgr  27462  frgrwopreglem4a  27481  h1de2ctlem  28738  spansn  28742  elspansn  28749  elspansn2  28750  spansneleq  28753  h1datom  28765  spansnj  28830  spansncv  28836  superpos  29537  sumdmdlem2  29602  aciunf1lem  29785  dfcnv2  29799  gsummpt2co  30101  locfinreflem  30228  esum2dlem  30475  sibfima  30721  sibfof  30723  bnj1373  31416  bnj1489  31442  cvmscbv  31558  cvmsdisj  31570  cvmsss2  31574  cvmliftlem15  31598  cvmlift2lem11  31613  cvmlift2lem12  31614  cvmlift2lem13  31615  mvtinf  31770  eldm3  31968  elima4  31994  conway  32226  scutval  32227  scutcut  32228  scutbday  32229  scutun12  32233  scutbdaybnd  32237  scutbdaylt  32238  fvsingle  32343  snelsingles  32345  dfiota3  32346  brapply  32361  funpartlem  32365  altopeq12  32385  ranksng  32590  neibastop3  32673  tailval  32684  filnetlem4  32692  bj-restsnss  33342  bj-restsnss2  33343  f1omptsnlem  33495  f1omptsn  33496  mptsnun  33498  dissneqlem  33499  dissneq  33500  lindsenlbs  33712  poimirlem4  33721  poimirlem25  33742  poimirlem26  33743  poimirlem27  33744  poimirlem31  33748  poimirlem32  33749  heiborlem3  33918  ismrer1  33943  lshpnel2N  34760  lsatlspsn2  34767  lsatlspsn  34768  lsatspn0  34775  lkrscss  34873  lfl1dim  34896  lfl1dim2N  34897  ldualvs  34912  atpointN  35518  watvalN  35768  trnsetN  35931  dih1dimatlem  37104  dihatexv  37113  dihjat1lem  37203  dihjat1  37204  lcfl7N  37276  lcfl8  37277  lcfl9a  37280  lcfrlem8  37324  lcfrlem9  37325  lcf1o  37326  mapdval2N  37405  mapdval4N  37407  mapdspex  37443  mapdn0  37444  mapdpglem23  37469  mapdpg  37481  mapdindp1  37495  mapdheq  37503  hvmapval  37535  mapdh9a  37564  hdmap1eq  37576  hdmap1cbv  37577  hdmapval  37603  hdmap10  37615  hdmaplkr  37688  mzpclval  37784  mzpcl1  37788  wopprc  38092  dnnumch3lem  38111  aomclem8  38126  mendvsca  38256  cytpval  38282  k0004lem3  38941  dvconstbi  39027  wessf1ornlem  39854  dvmptfprodlem  40633  fourierdlem32  40829  fourierdlem33  40830  fourierdlem48  40844  funressnmo  41659  aiotajust  41662  funressndmafv2rn  41806  fzopredsuc  41902  elsprel  42287  irinitoringc  42631  opeliun2xp  42673  dmmpt2ssx2  42677  lindslinindsimp2  42814  ldepspr  42824  ldepsnlinc  42859
  Copyright terms: Public domain W3C validator