Theorem sneq 4586

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 2743	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2797	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4577	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4577	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2791	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1541  {cab 2709  {csn 4576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-sn 4577

This theorem is referenced by:  sneqi  4587  sneqd  4588  euabsn  4679  absneu  4681  preq1  4686  tpeq3  4697  issn  4784  mosneq  4794  sneqbg  4795  opeq1  4825  snexg  5373  propeqop  5447  opthwiener  5454  otiunsndisj  5460  opeliunxp  5683  opeliun2xp  5684  relop  5790  inisegn0  6047  xpdifid  6115  dmsnsnsn  6167  predeq123  6249  iotajust  6436  iotanul2  6454  fconstg  6710  f1osng  6804  opabiotafun  6902  fvn0ssdmfun  7007  fsng  7070  fsn2g  7071  fnressn  7091  fressnfv  7093  funfvima3  7170  f12dfv  7207  f13dfv  7208  isofrlem  7274  isoselem  7275  elxp4  7852  elxp5  7853  1stval  7923  2ndval  7924  2ndval2  7939  fo1st  7941  fo2nd  7942  f1stres  7945  f2ndres  7946  mpomptsx  7996  dmmpossx  7998  fmpox  7999  ovmptss  8023  fparlem3  8044  fparlem4  8045  xpord2pred  8075  xpord3pred  8082  suppval  8092  suppsnop  8108  ressuppssdif  8115  brtpos2  8162  dftpos4  8175  tpostpos  8176  naddcllem  8591  eceq1  8661  fvdiagfn  8815  mapsncnv  8817  elixpsn  8861  ixpsnf1o  8862  ensn1g  8944  en1  8946  difsnen  8972  xpsneng  8975  xpcomco  8980  xpassen  8984  xpdom2  8985  canth2  9043  rexdif1en  9070  cnvfi  9085  marypha2lem2  9320  cardsn  9862  pm54.43  9894  dfac5lem3  10016  dfac5lem4  10017  dfac5lem4OLD  10019  kmlem9  10050  kmlem11  10052  kmlem12  10053  ackbij1lem8  10117  r1om  10134  fictb  10135  hsmexlem4  10320  axcc2lem  10327  axcc2  10328  axdc3lem4  10344  fpwwe2cbv  10521  fpwwe2lem3  10524  fpwwecbv  10535  canth4  10538  s3iunsndisj  14875  fsum2dlem  15677  fsumcnv  15680  fsumcom2  15681  ackbijnn  15735  fprod2dlem  15887  fprodcnv  15890  fprodcom2  15891  lcmfunsnlem1  16548  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  lcmfunsnlem2  16551  lcmfunsn  16555  vdwlem1  16893  vdwlem12  16904  vdwlem13  16905  vdwnn  16910  0ram  16932  ramz2  16936  pwsval  17390  symg2bas  19306  symgfixelsi  19348  pmtrfv  19365  pmtrprfval  19400  sylow2a  19532  efgrelexlema  19662  gsum2dlem2  19884  gsum2d2  19887  gsumcom2  19888  dprdcntz  19923  dprddisj  19924  dprd2dlem2  19955  dprd2dlem1  19956  dprd2da  19957  ablfac1eu  19988  ablfaclem3  20002  lssats2  20934  lspsneq0  20946  lbsind  21015  lspsneq  21060  lspdisj2  21065  lspsnsubn0  21078  lspprat  21091  islbs2  21092  lbsextlem4  21099  lbsextg  21100  lpi0  21264  lpi1  21265  irinitoringc  21417  pzriprnglem13  21431  pzriprnglem14  21432  frlmlbs  21735  lindfind  21754  lindsind  21755  lindfrn  21759  psrvsca  21887  evlssca  22025  mpfind  22043  coe1fv  22120  coe1tm  22188  pf1ind  22271  submaval  22497  mdetunilem3  22530  mdetunilem4  22531  mdetunilem9  22536  islp  23056  perfi  23071  t1sncld  23242  bwth  23326  dis2ndc  23376  nllyi  23391  dissnlocfin  23445  ptbasfi  23497  txkgen  23568  xkofvcn  23600  xkoinjcn  23603  qtopeu  23632  txswaphmeolem  23720  pt1hmeo  23722  elflim2  23880  cnextfvval  23981  cnextcn  23983  cnextfres1  23984  cnextfres  23985  tsmsxplem1  24069  tsmsxplem2  24070  ucncn  24200  itg11  25620  i1faddlem  25622  i1fmullem  25623  itg1addlem3  25627  itg1mulc  25633  eldv  25827  ply1lpir  26115  areambl  26896  conway  27741  scutval  27742  scutcut  27743  scutbday  27746  eqscut  27747  eqscut2  27748  scutun12  27752  scutbdaybnd  27757  scutbdaybnd2  27758  scutbdaylt  27760  eqscut3  27766  bday1s  27776  cuteq0  27777  cuteq1  27779  madebdaylemlrcut  27845  cofcut1  27865  cofcutr  27869  onsiso  28206  bdayn0p1  28295  expsval  28349  pw2cut2  28383  tglngval  28530  edglnl  29122  nbgrval  29315  nbgr2vtx1edg  29329  nbuhgr2vtx1edgb  29331  nbgr1vtx  29337  nb3grprlem2  29360  uvtxel  29367  uvtxel1  29375  uvtxusgrel  29382  cusgredg  29403  cplgr1v  29409  cplgr3v  29414  usgredgsscusgredg  29439  vtxdgval  29448  1loopgrvd2  29483  wlk1walk  29618  wlkres  29648  wlkp1lem8  29658  usgr2pthlem  29742  crctcshwlkn0lem6  29794  2wspiundisj  29942  clwwlknon1  30075  1wlkdlem4  30118  eupth2lem3lem3  30208  frcond1  30244  frgr1v  30249  nfrgr2v  30250  frgr3v  30253  1vwmgr  30254  3vfriswmgr  30256  3cyclfrgrrn1  30263  n4cyclfrgr  30269  frgrwopreglem4a  30288  h1de2ctlem  31533  spansn  31537  elspansn  31544  elspansn2  31545  spansneleq  31548  h1datom  31560  spansnj  31625  spansncv  31631  superpos  32332  sumdmdlem2  32397  aciunf1lem  32642  fnpreimac  32651  dfcnv2  32656  pwrssmgc  32979  gsummpt2co  33026  gsumpart  33035  gsumwrd2dccatlem  33044  gsumwrd2dccat  33045  0nellinds  33333  lindssn  33341  lsmsnidl  33362  nsgmgclem  33374  nsgmgc  33375  nsgqusf1olem1  33376  nsgqusf1olem2  33377  nsgqusf1olem3  33378  pidlnzb  33385  elrspunidl  33391  lbslsat  33627  lindsunlem  33635  extdgval  33664  fldextrspunlsplem  33684  locfinreflem  33851  esum2dlem  34103  sibfima  34349  sibfof  34351  bnj1373  35040  bnj1489  35066  funen1cnv  35098  fineqvac  35137  cplgredgex  35163  pfxwlk  35166  revwlk  35167  loop1cycl  35179  cvmscbv  35300  cvmsdisj  35312  cvmsss2  35316  cvmliftlem15  35340  cvmlift2lem11  35355  cvmlift2lem12  35356  cvmlift2lem13  35357  satffunlem1lem1  35444  satffunlem2lem1  35446  mvtinf  35597  eldm3  35803  elima4  35818  fvsingle  35960  snelsingles  35962  dfiota3  35963  brapply  35978  funpartlem  35982  altopeq12  36002  ranksng  36207  neibastop3  36402  tailval  36413  filnetlem4  36421  bj-snexg  37074  bj-restsnss  37123  bj-restsnss2  37124  f1omptsnlem  37376  f1omptsn  37377  mptsnun  37379  dissneqlem  37380  dissneq  37381  fvineqsnf1  37450  lindsadd  37659  lindsenlbs  37661  poimirlem4  37670  poimirlem25  37691  poimirlem26  37692  poimirlem27  37693  poimirlem31  37697  poimirlem32  37698  heiborlem3  37859  ismrer1  37884  lshpnel2N  39030  lsatlspsn2  39037  lsatlspsn  39038  lsatspn0  39045  lkrscss  39143  lfl1dim  39166  lfl1dim2N  39167  ldualvs  39182  atpointN  39788  watvalN  40038  trnsetN  40201  dih1dimatlem  41374  dihatexv  41383  dihjat1lem  41473  dihjat1  41474  lcfl7N  41546  lcfl8  41547  lcfl9a  41550  lcfrlem8  41594  lcfrlem9  41595  lcf1o  41596  mapdval2N  41675  mapdval4N  41677  mapdspex  41713  mapdn0  41714  mapdpglem23  41739  mapdpg  41751  mapdindp1  41765  mapdheq  41773  hvmapval  41805  mapdh9a  41834  hdmap1eq  41846  hdmap1cbv  41847  hdmapval  41873  hdmap10  41885  hdmaplkr  41958  sn-iotalem  42260  evlsvvval  42602  evlsevl  42610  0prjspnrel  42666  mzpclval  42764  mzpcl1  42768  wopprc  43069  dnnumch3lem  43085  aomclem8  43100  mendvsca  43226  cytpval  43241  snen1g  43563  k0004lem3  44188  dvconstbi  44373  relpfrlem  44992  permaxinf2lem  45051  wessf1ornlem  45228  dvmptfprodlem  45988  fourierdlem32  46183  fourierdlem33  46184  fourierdlem48  46198  funressnmo  47083  aiotajust  47121  funressndmafv2rn  47260  fzopredsuc  47360  elsprel  47512  clnbgrval  47859  dfvopnbgr2  47890  vopnbgrel  47891  dfclnbgr6  47893  dfnbgr6  47894  cycl3grtri  47984  dmmpossx2  48374  lindslinindsimp2  48501  ldepspr  48511  ldepsnlinc  48546  line  48770  rrxline  48772  dftpos5  48911  tposideq  48925  initc  49129  setc2othin  49504  functermceu  49548  idfudiag1  49563  funcsn  49579  0fucterm  49581  mndtcval  49617  mndtcbas  49619