Theorem sneq 4594

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 2775	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2829	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4589	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4589	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2823	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {cab 2741  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-sn 4589

This theorem is used by:  sneqi  4595  sneqd  4596  euabsn  4689  absneu  4691  preq1  4696  tpeq3  4707  issn  4792  mosneq  4802  sneqbg  4803  opeq1  4845  snexgALT  5406  propeqop  5486  opthwiener  5494  otiunsndisj  5500  opeliunxp  5725  opeliun2xp  5726  relop  5838  inisegn0  6114  xpdifid  6177  xpdifcnvepel  6178  dmsnsnsn  6240  predeq123  6331  iotajust  6519  iotanul2  6537  fconstg  6799  f1osng  6898  opabiotafun  6996  fvn0ssdmfun  7106  fsng  7170  fsn2g  7171  fnressn  7194  fressnfv  7196  funfvima3  7273  f12dfv  7312  f13dfv  7313  isofrlem  7379  isoselem  7380  elxp4  7968  elxp5  7969  1stval  8037  2ndval  8038  2ndval2  8053  fo1st  8055  fo2nd  8056  f1stres  8059  f2ndres  8060  mpomptsx  8110  dmmpossx  8112  fmpox  8113  ovmptssOLD  8140  fparlem3  8162  fparlem4  8163  xpord2pred  8199  xpord3pred  8206  suppval  8216  suppsnop  8233  ressuppssdif  8240  brtpos2  8287  dftpos4  8300  tpostpos  8301  naddcllem  8723  eceq1  8795  fvdiagfn  8957  mapsncnv  8959  elixpsn  9003  ixpsnf1o  9004  ensn1g  9087  en1  9089  funen1cnv  9094  difsnen  9116  xpsneng  9119  xpcomco  9124  xpassen  9128  xpdom2  9129  canth2  9187  rexdif1en  9214  cnvfi  9229  marypha2lem2  9465  ranksng  9911  cardsn  10087  pm54.43  10121  dfac5lem3  10243  dfac5lem4  10244  kmlem9  10276  kmlem11  10278  kmlem12  10279  ackbij1lem8  10343  hfom  10360  fictb  10361  hsmexlem4  10546  axcc2lem  10553  axcc2  10554  axdc3lem4  10570  fpwwe2cbv  10754  fpwwe2lem3  10757  fpwwecbv  10768  canth4  10771  s3iunsndisj  15164  fsum2dlem  15980  fsumcnv  15983  fsumcom2  15984  ackbijnn  16041  fprod2dlem  16191  fprodcnv  16194  fprodcom2  16195  lcmfunsnlem1  16856  lcmfunsnlem2lem1  16857  lcmfunsnlem2lem2  16858  lcmfunsnlem2  16859  lcmfunsn  16863  vdwlem1  17203  vdwlem12  17214  vdwlem13  17215  vdwnn  17220  0ram  17242  ramz2  17246  pwsval  17707  symg2bas  19658  symgfixelsi  19700  pmtrfv  19717  pmtrprfval  19752  sylow2a  19884  efgrelexlema  20014  gsum2dlem2  20236  gsum2d2  20239  gsumcom2  20240  dprdcntz  20275  dprddisj  20276  dprd2dlem2  20307  dprd2dlem1  20308  dprd2da  20309  ablfac1eu  20340  ablfaclem3  20354  lssats2  21326  lspsneq0  21338  lbsind  21406  lspsneq  21451  lspdisj2  21456  lspsnsubn0  21469  lspprat  21482  islbs2  21483  lbsextlem4  21490  lbsextg  21491  lpi0  21701  lpi1  21702  irinitoringc  21840  pzriprnglem13  21854  pzriprnglem14  21855  frlmlbs  22158  lindfind  22177  lindsind  22178  lindfrn  22182  lindsenlbs  22212  psrvsca  22312  evlsvvval  22457  evlssca  22458  mpfind  22479  evlsevl  22496  coe1fv  22579  coe1tm  22647  pf1ind  22728  submaval  22951  mdetunilem3  22984  mdetunilem4  22985  mdetunilem9  22990  islp  23513  perfi  23528  t1sncld  23699  bwth  23783  dis2ndc  23834  nllyi  23849  dissnlocfin  23903  ptbasfi  23955  txkgen  24026  xkofvcn  24058  xkoinjcn  24061  qtopeu  24090  txswaphmeolem  24178  pt1hmeo  24180  elflim2  24338  cnextfvval  24439  cnextcn  24441  cnextfres1  24442  cnextfres  24443  tsmsxplem1  24527  tsmsxplem2  24528  ucncn  24658  itg11  26067  i1faddlem  26069  i1fmullem  26070  itg1addlem3  26074  itg1mulc  26080  eldv  26273  ply1lpir  26555  areambl  27343  conway  28222  cutsval  28223  cutcuts  28224  cutbday  28227  eqcuts  28228  eqcuts2  28229  cutsun12  28233  cutbdaybnd  28238  cutbdaybnd2  28239  cutbdaylt  28241  eqcuts3  28247  bday1  28257  cuteq0  28258  cuteq1  28260  madebdaylemlrcut  28342  sltsbday  28360  cofcut1  28363  cofcutr  28367  oniso  28714  bdayn0p1  28812  expsval  28868  pw2cut2  28905  tglngval  29071  edglnl  29778  nbgrval  29974  nbgr2vtx1edg  29988  nbuhgr2vtx1edgb  29990  nbgr1vtx  29996  nb3grprlem2  30019  uvtxel  30026  uvtxel1  30034  uvtxusgrel  30041  cusgredg  30062  cplgr1v  30068  cplgr3v  30073  usgredgsscusgredg  30097  vtxdgval  30106  1loopgrvd2  30141  wlk1walk  30276  wlkres  30306  wlkp1lem8  30316  pfxwlk  30323  revwlk  30324  usgr2pthlem  30406  crctcshwlkn0lem6  30461  2wspiundisj  30612  clwwlknon1  30745  1wlkdlem4  30788  loop1cycl  30801  eupth2lem3lem3  30888  frcond1  30924  frgr1v  30929  nfrgr2v  30930  frgr3v  30933  1vwmgr  30934  3vfriswmgr  30936  3cyclfrgrrn1  30943  n4cyclfrgr  30949  frgrwopreglem4a  30968  h1de2ctlem  32214  spansn  32218  elspansn  32225  elspansn2  32226  spansneleq  32229  h1datom  32241  spansnj  32306  spansncv  32312  superpos  33013  sumdmdlem2  33078  aciunf1lem  33354  fnpreimac  33362  dfcnv2  33366  pwrssmgc  33660  gsummpt2co  33708  gsumpart  33723  gsumwrd2dccatlem  33737  gsumwrd2dccat  33738  edompid  33961  0nellinds  34030  lindssn  34037  lsmsnidl  34056  nsgmgclem  34066  nsgmgc  34067  nsgqusf1olem1  34068  nsgqusf1olem2  34069  nsgqusf1olem3  34070  pidlnzb  34076  elrspunidl  34082  extvfval  34275  esplyfval1  34316  esplyfvaln  34317  lbslsat  34359  lindsunlem  34367  extdgval  34396  fldextrspunlsplem  34416  locfinreflem  34583  esum2dlem  34835  sibfima  35081  sibfof  35083  bnj1373  35771  bnj1489  35797  fineqvac  35925  onvfowev  36091  cplgredgex  36103  cvmscbv  36231  cvmsdisj  36243  cvmsss2  36247  cvmliftlem15  36271  cvmlift2lem11  36286  cvmlift2lem12  36287  cvmlift2lem13  36288  satffunlem1lem1  36375  satffunlem2lem1  36377  mvtinf  36528  eldm3  36741  elima4  36755  fvsingle  36897  snelsingles  36899  dfiota3  36900  brapply  36915  funpartlem  36921  altopeq12  36942  neibastop3  37365  tailval  37376  filnetlem4  37384  ttcid  37495  mh-inf3sn  37545  mh-infprim2bi  37550  mh-infprim3bi  37551  bj-snexg  38162  bj-restsnss  38274  bj-restsnss2  38275  f1omptsnlem  38527  f1omptsn  38528  mptsnun  38530  dissneqlem  38531  dissneq  38532  fvineqsnf1  38601  lindsadd  38804  poimirlem4  38810  poimirlem25  38831  poimirlem26  38832  poimirlem27  38833  poimirlem31  38837  poimirlem32  38838  heiborlem3  39013  ismrer1  39038  lshpnel2N  40308  lsatlspsn2  40315  lsatlspsn  40316  lsatspn0  40323  lkrscss  40421  lfl1dim  40444  lfl1dim2N  40445  ldualvs  40460  atpointN  41066  watvalN  41316  trnsetN  41479  dih1dimatlem  42652  dihatexv  42661  dihjat1lem  42751  dihjat1  42752  lcfl7N  42824  lcfl8  42825  lcfl9a  42828  lcfrlem8  42872  lcfrlem9  42873  lcf1o  42874  mapdval2N  42953  mapdval4N  42955  mapdspex  42991  mapdn0  42992  mapdpglem23  43017  mapdpg  43029  mapdindp1  43043  mapdheq  43051  hvmapval  43083  mapdh9a  43112  hdmap1eq  43124  hdmap1cbv  43125  hdmapval  43151  hdmap10  43163  hdmaplkr  43236  sn-iotalem  43542  0prjspnrel  43929  mzpclval  44002  mzpcl1  44006  wopprc  44303  dnnumch3lem  44319  aomclem8  44329  mendvsca  44450  cytpval  44465  snen1g  44786  k0004lem3  45410  dvconstbi  45579  relpfrlem  46207  permaxinf2lem  46266  ackbij3  46289  wessf1ornlem  46473  dvmptfprodlem  47227  fourierdlem32  47422  fourierdlem33  47423  fourierdlem48  47437  funressnmo  48389  aiotajust  48427  funressndmafv2rn  48566  fzopredsuc  48667  elsprel  48830  clnbgrval  49193  dfvopnbgr2  49224  vopnbgrel  49225  dfclnbgr6  49227  dfnbgr6  49228  cycl3grtri  49318  azval  49716  dmmpossx2  49780  lindslinindsimp2  49906  ldepspr  49916  ldepsnlinc  49951  line  50176  rrxline  50178  dftpos5  50318  tposideq  50332  initc  50537  setc2othin  50932  functermceu  50976  idfudiag1  50991  funcsn  51010  0fucterm  51012  mndtcval  51048  mndtcbaseu  51050