Theorem sneq 4577

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 2833	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2885	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4568	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4568	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2881	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1537  {cab 2799  {csn 4567

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 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-sn 4568

This theorem is referenced by:  sneqi  4578  sneqd  4579  euabsn  4662  absneu  4664  preq1  4669  tpeq3  4680  issn  4763  mosneq  4773  sneqbg  4774  opeq1  4803  propeqop  5397  opthwiener  5404  otiunsndisj  5410  opeliunxp  5619  relop  5721  elimasng  5955  inisegn0  5961  xpdifid  6025  dmsnsnsn  6077  predeq123  6149  suceq  6256  iotajust  6313  fconstg  6566  f1osng  6655  opabiotafun  6744  fvn0ssdmfun  6842  fsng  6899  fsn2g  6900  fnressn  6920  fressnfv  6922  funfvima3  6998  f12dfv  7030  f13dfv  7031  isofrlem  7093  isoselem  7094  elxp4  7627  elxp5  7628  1stval  7691  2ndval  7692  2ndval2  7707  fo1st  7709  fo2nd  7710  f1stres  7713  f2ndres  7714  mpomptsx  7762  dmmpossx  7764  fmpox  7765  ovmptss  7788  fparlem3  7809  fparlem4  7810  suppval  7832  suppsnop  7844  ressuppssdif  7851  brtpos2  7898  dftpos4  7911  tpostpos  7912  eceq1  8327  fvdiagfn  8455  mapsncnv  8457  elixpsn  8501  ixpsnf1o  8502  ensn1g  8574  en1  8576  difsnen  8599  xpsneng  8602  xpcomco  8607  xpassen  8611  xpdom2  8612  canth2  8670  phplem3  8698  xpfi  8789  marypha2lem2  8900  cardsn  9398  pm54.43  9429  dfac5lem3  9551  dfac5lem4  9552  kmlem9  9584  kmlem11  9586  kmlem12  9587  ackbij1lem8  9649  r1om  9666  fictb  9667  hsmexlem4  9851  axcc2lem  9858  axcc2  9859  axdc3lem4  9875  fpwwe2cbv  10052  fpwwe2lem3  10055  fpwwecbv  10066  canth4  10069  s3iunsndisj  14328  fsum2dlem  15125  fsumcnv  15128  fsumcom2  15129  ackbijnn  15183  fprod2dlem  15334  fprodcnv  15337  fprodcom2  15338  lcmfunsnlem1  15981  lcmfunsnlem2lem1  15982  lcmfunsnlem2lem2  15983  lcmfunsnlem2  15984  lcmfunsn  15988  vdwlem1  16317  vdwlem12  16328  vdwlem13  16329  vdwnn  16334  0ram  16356  ramz2  16360  pwsval  16759  symg2bas  18521  symgfixelsi  18563  pmtrfv  18580  pmtrprfval  18615  sylow2a  18744  efgrelexlema  18875  gsum2dlem2  19091  gsum2d2  19094  gsumcom2  19095  dprdcntz  19130  dprddisj  19131  dprd2dlem2  19162  dprd2dlem1  19163  dprd2da  19164  ablfac1eu  19195  ablfaclem3  19209  lssats2  19772  lspsneq0  19784  lbsind  19852  lspsneq  19894  lspdisj2  19899  lspsnsubn0  19912  lspprat  19925  islbs2  19926  lbsextlem4  19933  lbsextg  19934  lpi0  20020  lpi1  20021  psrvsca  20171  evlssca  20302  mpfind  20320  coe1fv  20374  coe1tm  20441  pf1ind  20518  frlmlbs  20941  lindfind  20960  lindsind  20961  lindfrn  20965  submaval  21190  mdetunilem3  21223  mdetunilem4  21224  mdetunilem9  21229  islp  21748  perfi  21763  t1sncld  21934  bwth  22018  dis2ndc  22068  nllyi  22083  dissnlocfin  22137  ptbasfi  22189  txkgen  22260  xkofvcn  22292  xkoinjcn  22295  qtopeu  22324  txswaphmeolem  22412  pt1hmeo  22414  elflim2  22572  cnextfvval  22673  cnextcn  22675  cnextfres1  22676  cnextfres  22677  tsmsxplem1  22761  tsmsxplem2  22762  ucncn  22894  itg11  24292  i1faddlem  24294  i1fmullem  24295  itg1addlem3  24299  itg1mulc  24305  eldv  24496  ply1lpir  24772  areambl  25536  tglngval  26337  edglnl  26928  nbgrval  27118  nbgr2vtx1edg  27132  nbuhgr2vtx1edgb  27134  nbgr1vtx  27140  nb3grprlem2  27163  uvtxel  27170  uvtxel1  27178  uvtxusgrel  27185  cusgredg  27206  cplgr1v  27212  cplgr3v  27217  usgredgsscusgredg  27241  vtxdgval  27250  1loopgrvd2  27285  wlk1walk  27420  wlkres  27452  wlkp1lem8  27462  usgr2pthlem  27544  crctcshwlkn0lem6  27593  2wspiundisj  27742  clwwlknon1  27876  1wlkdlem4  27919  eupth2lem3lem3  28009  frcond1  28045  frgr1v  28050  nfrgr2v  28051  frgr3v  28054  1vwmgr  28055  3vfriswmgr  28057  3cyclfrgrrn1  28064  n4cyclfrgr  28070  frgrwopreglem4a  28089  h1de2ctlem  29332  spansn  29336  elspansn  29343  elspansn2  29344  spansneleq  29347  h1datom  29359  spansnj  29424  spansncv  29430  superpos  30131  sumdmdlem2  30196  aciunf1lem  30407  fnpreimac  30416  dfcnv2  30422  gsummpt2co  30686  0nellinds  30935  lindssn  30939  lsmsnidl  30949  lbslsat  31014  lindsunlem  31020  extdgval  31044  locfinreflem  31104  esum2dlem  31351  sibfima  31596  sibfof  31598  bnj1373  32302  bnj1489  32328  funen1cnv  32357  cplgredgex  32367  pfxwlk  32370  revwlk  32371  loop1cycl  32384  cvmscbv  32505  cvmsdisj  32517  cvmsss2  32521  cvmliftlem15  32545  cvmlift2lem11  32560  cvmlift2lem12  32561  cvmlift2lem13  32562  satffunlem1lem1  32649  satffunlem2lem1  32651  mvtinf  32802  eldm3  32997  elima4  33019  conway  33264  scutval  33265  scutcut  33266  scutbday  33267  scutun12  33271  scutbdaybnd  33275  scutbdaylt  33276  fvsingle  33381  snelsingles  33383  dfiota3  33384  brapply  33399  funpartlem  33403  altopeq12  33423  ranksng  33628  neibastop3  33710  tailval  33721  filnetlem4  33729  bj-restsnss  34377  bj-restsnss2  34378  f1omptsnlem  34620  f1omptsn  34621  mptsnun  34623  dissneqlem  34624  dissneq  34625  fvineqsnf1  34694  lindsadd  34900  lindsenlbs  34902  poimirlem4  34911  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem31  34938  poimirlem32  34939  heiborlem3  35106  ismrer1  35131  lshpnel2N  36136  lsatlspsn2  36143  lsatlspsn  36144  lsatspn0  36151  lkrscss  36249  lfl1dim  36272  lfl1dim2N  36273  ldualvs  36288  atpointN  36894  watvalN  37144  trnsetN  37307  dih1dimatlem  38480  dihatexv  38489  dihjat1lem  38579  dihjat1  38580  lcfl7N  38652  lcfl8  38653  lcfl9a  38656  lcfrlem8  38700  lcfrlem9  38701  lcf1o  38702  mapdval2N  38781  mapdval4N  38783  mapdspex  38819  mapdn0  38820  mapdpglem23  38845  mapdpg  38857  mapdindp1  38871  mapdheq  38879  hvmapval  38911  mapdh9a  38940  hdmap1eq  38952  hdmap1cbv  38953  hdmapval  38979  hdmap10  38991  hdmaplkr  39064  0prjspnrel  39289  mzpclval  39342  mzpcl1  39346  wopprc  39647  dnnumch3lem  39666  aomclem8  39681  mendvsca  39811  cytpval  39829  snen1g  39910  k0004lem3  40519  dvconstbi  40686  wessf1ornlem  41465  dvmptfprodlem  42249  fourierdlem32  42444  fourierdlem33  42445  fourierdlem48  42459  funressnmo  43301  aiotajust  43304  funressndmafv2rn  43442  fzopredsuc  43543  elsprel  43657  irinitoringc  44360  opeliun2xp  44401  dmmpossx2  44405  lindslinindsimp2  44538  ldepspr  44548  ldepsnlinc  44583  line  44739  rrxline  44741