Theorem sneq 4187

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.

Step	Hyp	Ref	Expression
1		eqeq2 2633	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2741	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4178	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4178	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2681	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1483  {cab 2608  {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-sn 4178

This theorem is referenced by:  sneqi  4188  sneqd  4189  euabsn  4261  absneu  4263  preq1  4268  tpeq3  4279  snssg  4327  issn  4363  sneqrgOLD  4373  sneqbg  4374  opeq1  4402  unisng  4452  propeqop  4970  opthwiener  4976  otiunsndisj  4980  opeliunxp  5170  relop  5272  elimasng  5491  inisegn0  5497  xpdifid  5562  dmsnsnsn  5613  predeq123  5681  suceq  5790  iotajust  5850  fconstg  6092  f1osng  6177  opabiotafun  6259  fvn0ssdmfun  6350  fsng  6404  fsn2g  6405  fnressn  6425  fressnfv  6427  funfvima3  6495  f12dfv  6529  f13dfv  6530  isofrlem  6590  isoselem  6591  snnexOLD  6967  elxp4  7110  elxp5  7111  1stval  7170  2ndval  7171  2ndval2  7186  fo1st  7188  fo2nd  7189  f1stres  7190  f2ndres  7191  mpt2mptsx  7233  dmmpt2ssx  7235  fmpt2x  7236  ovmptss  7258  fparlem3  7279  fparlem4  7280  suppval  7297  suppsnop  7309  ressuppssdif  7316  brtpos2  7358  dftpos4  7371  tpostpos  7372  eceq1  7782  fvdiagfn  7902  mapsncnv  7904  elixpsn  7947  ixpsnf1o  7948  ensn1g  8021  en1  8023  difsnen  8042  xpsneng  8045  xpcomco  8050  xpassen  8054  xpdom2  8055  canth2  8113  phplem3  8141  xpfi  8231  marypha2lem2  8342  cardsn  8795  pm54.43  8826  dfac5lem3  8948  dfac5lem4  8949  kmlem9  8980  kmlem11  8982  kmlem12  8983  ackbij1lem8  9049  r1om  9066  fictb  9067  hsmexlem4  9251  axcc2lem  9258  axcc2  9259  axdc3lem4  9275  fpwwe2cbv  9452  fpwwe2lem3  9455  fpwwecbv  9466  canth4  9469  s3iunsndisj  13707  fsum2dlem  14501  fsumcnv  14504  fsumcom2  14505  fsumcom2OLD  14506  ackbijnn  14560  fprod2dlem  14710  fprodcnv  14713  fprodcom2  14714  fprodcom2OLD  14715  lcmfunsnlem1  15350  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  lcmfunsnlem2  15353  lcmfunsn  15357  vdwlem1  15685  vdwlem12  15696  vdwlem13  15697  vdwnn  15702  0ram  15724  ramz2  15728  pwsval  16146  xpsfval  16227  xpsval  16232  symg2bas  17818  symgfixelsi  17855  pmtrfv  17872  pmtrprfval  17907  sylow2a  18034  efgrelexlema  18162  gsum2dlem2  18370  gsum2d2  18373  gsumcom2  18374  dprdcntz  18407  dprddisj  18408  dprd2dlem2  18439  dprd2dlem1  18440  dprd2da  18441  ablfac1eu  18472  ablfaclem3  18486  lssats2  19000  lspsneq0  19012  lbsind  19080  lspsneq  19122  lspdisj2  19127  lspsnsubn0  19140  lspprat  19153  islbs2  19154  lbsextlem4  19161  lbsextg  19162  lpi0  19247  lpi1  19248  psrvsca  19391  evlssca  19522  mpfind  19536  coe1fv  19576  coe1tm  19643  pf1ind  19719  frlmlbs  20136  lindfind  20155  lindsind  20156  lindfrn  20160  submaval  20387  mdetunilem3  20420  mdetunilem4  20421  mdetunilem9  20426  islp  20944  perfi  20959  t1sncld  21130  bwth  21213  dis2ndc  21263  nllyi  21278  dissnlocfin  21332  ptbasfi  21384  txkgen  21455  xkofvcn  21487  xkoinjcn  21490  qtopeu  21519  txswaphmeolem  21607  pt1hmeo  21609  elflim2  21768  cnextfvval  21869  cnextcn  21871  cnextfres1  21872  cnextfres  21873  tsmsxplem1  21956  tsmsxplem2  21957  ucncn  22089  itg11  23458  i1faddlem  23460  i1fmullem  23461  itg1addlem3  23465  itg1mulc  23471  eldv  23662  ply1lpir  23938  areambl  24685  tglngval  25446  edglnl  26038  nbgrval  26234  nbgr2vtx1edg  26246  nbuhgr2vtx1edgb  26248  nbgr1vtx  26254  nb3grprlem2  26283  uvtxael  26288  uvtxael1  26296  uvtxusgrel  26304  cusgredg  26320  cplgr1v  26326  cplgr3v  26331  usgredgsscusgredg  26355  vtxdgval  26364  1loopgrvd2  26399  wlk1walk  26535  wlkres  26567  wlkp1lem8  26577  usgr2pthlem  26659  crctcshwlkn0lem6  26707  2wspiundisj  26856  1wlkdlem4  27000  eupth2lem3lem3  27090  frcond1  27130  frgr1v  27135  nfrgr2v  27136  frgr3v  27139  1vwmgr  27140  3vfriswmgr  27142  3cyclfrgrrn1  27149  n4cyclfrgr  27155  frgrwopreglem4a  27174  h1de2ctlem  28414  spansn  28418  elspansn  28425  elspansn2  28426  spansneleq  28429  h1datom  28441  spansnj  28506  spansncv  28512  superpos  29213  sumdmdlem2  29278  aciunf1lem  29462  dfcnv2  29476  gsummpt2co  29780  locfinreflem  29907  esum2dlem  30154  sibfima  30400  sibfof  30402  bnj1373  31098  bnj1489  31124  cvmscbv  31240  cvmsdisj  31252  cvmsss2  31256  cvmliftlem15  31280  cvmlift2lem11  31295  cvmlift2lem12  31296  cvmlift2lem13  31297  mvtinf  31452  eldm3  31651  elima4  31679  conway  31910  scutval  31911  scutcut  31912  scutbday  31913  scutun12  31917  scutbdaybnd  31921  scutbdaylt  31922  fvsingle  32027  snelsingles  32029  dfiota3  32030  brapply  32045  funpartlem  32049  altopeq12  32069  ranksng  32274  neibastop3  32357  tailval  32368  filnetlem4  32376  bj-restsnss  33036  bj-restsnss2  33037  f1omptsnlem  33183  f1omptsn  33184  mptsnun  33186  dissneqlem  33187  dissneq  33188  lindsenlbs  33404  poimirlem4  33413  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem31  33440  poimirlem32  33441  heiborlem3  33612  ismrer1  33637  lshpnel2N  34272  lsatlspsn2  34279  lsatlspsn  34280  lsatspn0  34287  lkrscss  34385  lfl1dim  34408  lfl1dim2N  34409  ldualvs  34424  atpointN  35029  watvalN  35279  trnsetN  35443  dih1dimatlem  36618  dihatexv  36627  dihjat1lem  36717  dihjat1  36718  lcfl7N  36790  lcfl8  36791  lcfl9a  36794  lcfrlem8  36838  lcfrlem9  36839  lcf1o  36840  mapdval2N  36919  mapdval4N  36921  mapdspex  36957  mapdn0  36958  mapdpglem23  36983  mapdpg  36995  mapdindp1  37009  mapdheq  37017  hvmapval  37049  mapdh9a  37079  hdmap1eq  37091  hdmap1cbv  37092  hdmapval  37120  hdmap10  37132  hdmaplkr  37205  mzpclval  37288  mzpcl1  37292  wopprc  37597  dnnumch3lem  37616  aomclem8  37631  mendvsca  37761  cytpval  37787  k0004lem3  38447  dvconstbi  38533  wessf1ornlem  39371  dvmptfprodlem  40159  fourierdlem32  40356  fourierdlem33  40357  fourierdlem48  40371  fzopredsuc  41333  elsprel  41725  irinitoringc  42069  opeliun2xp  42111  dmmpt2ssx2  42115  lindslinindsimp2  42252  ldepspr  42262  ldepsnlinc  42297