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

Theorem sneq 4220
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 2662 . . 3 (𝐴 = 𝐵 → (𝑥 = 𝐴𝑥 = 𝐵))
21abbidv 2770 . 2 (𝐴 = 𝐵 → {𝑥𝑥 = 𝐴} = {𝑥𝑥 = 𝐵})
3 df-sn 4211 . 2 {𝐴} = {𝑥𝑥 = 𝐴}
4 df-sn 4211 . 2 {𝐵} = {𝑥𝑥 = 𝐵}
52, 3, 43eqtr4g 2710 1 (𝐴 = 𝐵 → {𝐴} = {𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  {cab 2637  {csn 4210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-sn 4211
This theorem is referenced by:  sneqi  4221  sneqd  4222  euabsn  4293  absneu  4295  preq1  4300  tpeq3  4311  snssgOLD  4349  issn  4395  sneqrgOLD  4405  sneqbg  4406  opeq1  4433  unisng  4484  propeqop  4999  opthwiener  5005  otiunsndisj  5009  opeliunxp  5204  relop  5305  elimasng  5526  inisegn0  5532  xpdifid  5597  dmsnsnsn  5649  predeq123  5719  suceq  5828  iotajust  5888  fconstg  6130  f1osng  6215  opabiotafun  6298  fvn0ssdmfun  6390  fsng  6444  fsn2g  6445  fnressn  6465  fressnfv  6467  funfvima3  6535  f12dfv  6569  f13dfv  6570  isofrlem  6630  isoselem  6631  snnexOLD  7009  elxp4  7152  elxp5  7153  1stval  7212  2ndval  7213  2ndval2  7228  fo1st  7230  fo2nd  7231  f1stres  7234  f2ndres  7235  mpt2mptsx  7278  dmmpt2ssx  7280  fmpt2x  7281  ovmptss  7303  fparlem3  7324  fparlem4  7325  suppval  7342  suppsnop  7354  ressuppssdif  7361  brtpos2  7403  dftpos4  7416  tpostpos  7417  eceq1  7825  fvdiagfn  7944  mapsncnv  7946  elixpsn  7989  ixpsnf1o  7990  ensn1g  8062  en1  8064  difsnen  8083  xpsneng  8086  xpcomco  8091  xpassen  8095  xpdom2  8096  canth2  8154  phplem3  8182  xpfi  8272  marypha2lem2  8383  cardsn  8833  pm54.43  8864  dfac5lem3  8986  dfac5lem4  8987  kmlem9  9018  kmlem11  9020  kmlem12  9021  ackbij1lem8  9087  r1om  9104  fictb  9105  hsmexlem4  9289  axcc2lem  9296  axcc2  9297  axdc3lem4  9313  fpwwe2cbv  9490  fpwwe2lem3  9493  fpwwecbv  9504  canth4  9507  s3iunsndisj  13753  fsum2dlem  14545  fsumcnv  14548  fsumcom2  14549  fsumcom2OLD  14550  ackbijnn  14604  fprod2dlem  14754  fprodcnv  14757  fprodcom2  14758  fprodcom2OLD  14759  lcmfunsnlem1  15397  lcmfunsnlem2lem1  15398  lcmfunsnlem2lem2  15399  lcmfunsnlem2  15400  lcmfunsn  15404  vdwlem1  15732  vdwlem12  15743  vdwlem13  15744  vdwnn  15749  0ram  15771  ramz2  15775  pwsval  16193  xpsfval  16274  xpsval  16279  symg2bas  17864  symgfixelsi  17901  pmtrfv  17918  pmtrprfval  17953  sylow2a  18080  efgrelexlema  18208  gsum2dlem2  18416  gsum2d2  18419  gsumcom2  18420  dprdcntz  18453  dprddisj  18454  dprd2dlem2  18485  dprd2dlem1  18486  dprd2da  18487  ablfac1eu  18518  ablfaclem3  18532  lssats2  19048  lspsneq0  19060  lbsind  19128  lspsneq  19170  lspdisj2  19175  lspsnsubn0  19188  lspprat  19201  islbs2  19202  lbsextlem4  19209  lbsextg  19210  lpi0  19295  lpi1  19296  psrvsca  19439  evlssca  19570  mpfind  19584  coe1fv  19624  coe1tm  19691  pf1ind  19767  frlmlbs  20184  lindfind  20203  lindsind  20204  lindfrn  20208  submaval  20435  mdetunilem3  20468  mdetunilem4  20469  mdetunilem9  20474  islp  20992  perfi  21007  t1sncld  21178  bwth  21261  dis2ndc  21311  nllyi  21326  dissnlocfin  21380  ptbasfi  21432  txkgen  21503  xkofvcn  21535  xkoinjcn  21538  qtopeu  21567  txswaphmeolem  21655  pt1hmeo  21657  elflim2  21815  cnextfvval  21916  cnextcn  21918  cnextfres1  21919  cnextfres  21920  tsmsxplem1  22003  tsmsxplem2  22004  ucncn  22136  itg11  23503  i1faddlem  23505  i1fmullem  23506  itg1addlem3  23510  itg1mulc  23516  eldv  23707  ply1lpir  23983  areambl  24730  tglngval  25491  edglnl  26083  nbgrval  26274  nbgr2vtx1edg  26291  nbuhgr2vtx1edgb  26293  nbgr1vtx  26299  nb3grprlem2  26327  uvtxel  26335  uvtxaelOLD  26336  uvtxel1  26345  uvtxael1OLD  26347  uvtxusgrel  26354  cusgredg  26376  cplgr1v  26382  cplgr3v  26387  usgredgsscusgredg  26411  vtxdgval  26420  1loopgrvd2  26455  wlk1walk  26591  wlkres  26623  wlkp1lem8  26633  usgr2pthlem  26715  crctcshwlkn0lem6  26763  2wspiundisj  26930  clwwlknon1  27072  1wlkdlem4  27118  eupth2lem3lem3  27208  frcond1  27246  frgr1v  27251  nfrgr2v  27252  frgr3v  27255  1vwmgr  27256  3vfriswmgr  27258  3cyclfrgrrn1  27265  n4cyclfrgr  27271  frgrwopreglem4a  27290  h1de2ctlem  28542  spansn  28546  elspansn  28553  elspansn2  28554  spansneleq  28557  h1datom  28569  spansnj  28634  spansncv  28640  superpos  29341  sumdmdlem2  29406  aciunf1lem  29590  dfcnv2  29604  gsummpt2co  29908  locfinreflem  30035  esum2dlem  30282  sibfima  30528  sibfof  30530  bnj1373  31224  bnj1489  31250  cvmscbv  31366  cvmsdisj  31378  cvmsss2  31382  cvmliftlem15  31406  cvmlift2lem11  31421  cvmlift2lem12  31422  cvmlift2lem13  31423  mvtinf  31578  eldm3  31777  elima4  31803  conway  32035  scutval  32036  scutcut  32037  scutbday  32038  scutun12  32042  scutbdaybnd  32046  scutbdaylt  32047  fvsingle  32152  snelsingles  32154  dfiota3  32155  brapply  32170  funpartlem  32174  altopeq12  32194  ranksng  32399  neibastop3  32482  tailval  32493  filnetlem4  32501  bj-restsnss  33161  bj-restsnss2  33162  f1omptsnlem  33313  f1omptsn  33314  mptsnun  33316  dissneqlem  33317  dissneq  33318  lindsenlbs  33534  poimirlem4  33543  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  poimirlem31  33570  poimirlem32  33571  heiborlem3  33742  ismrer1  33767  lshpnel2N  34590  lsatlspsn2  34597  lsatlspsn  34598  lsatspn0  34605  lkrscss  34703  lfl1dim  34726  lfl1dim2N  34727  ldualvs  34742  atpointN  35347  watvalN  35597  trnsetN  35761  dih1dimatlem  36935  dihatexv  36944  dihjat1lem  37034  dihjat1  37035  lcfl7N  37107  lcfl8  37108  lcfl9a  37111  lcfrlem8  37155  lcfrlem9  37156  lcf1o  37157  mapdval2N  37236  mapdval4N  37238  mapdspex  37274  mapdn0  37275  mapdpglem23  37300  mapdpg  37312  mapdindp1  37326  mapdheq  37334  hvmapval  37366  mapdh9a  37396  hdmap1eq  37408  hdmap1cbv  37409  hdmapval  37437  hdmap10  37449  hdmaplkr  37522  mzpclval  37605  mzpcl1  37609  wopprc  37914  dnnumch3lem  37933  aomclem8  37948  mendvsca  38078  cytpval  38104  k0004lem3  38764  dvconstbi  38850  wessf1ornlem  39685  dvmptfprodlem  40477  fourierdlem32  40674  fourierdlem33  40675  fourierdlem48  40689  fzopredsuc  41658  elsprel  42050  irinitoringc  42394  opeliun2xp  42436  dmmpt2ssx2  42440  lindslinindsimp2  42577  ldepspr  42587  ldepsnlinc  42622
  Copyright terms: Public domain W3C validator