Theorem sneq 4571

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 2750	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2807	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4562	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4562	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2803	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1539  {cab 2715  {csn 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-sn 4562

This theorem is referenced by:  sneqi  4572  sneqd  4573  euabsn  4662  absneu  4664  preq1  4669  tpeq3  4680  issn  4763  mosneq  4773  sneqbg  4774  opeq1  4804  propeqop  5421  opthwiener  5428  otiunsndisj  5434  opeliunxp  5654  relop  5759  elimasngOLD  5998  inisegn0  6006  xpdifid  6071  dmsnsnsn  6123  predeq123  6203  suceq  6331  iotajust  6390  fconstg  6661  f1osng  6757  opabiotafun  6849  fvn0ssdmfun  6952  fsng  7009  fsn2g  7010  fnressn  7030  fressnfv  7032  funfvima3  7112  f12dfv  7145  f13dfv  7146  isofrlem  7211  isoselem  7212  elxp4  7769  elxp5  7770  1stval  7833  2ndval  7834  2ndval2  7849  fo1st  7851  fo2nd  7852  f1stres  7855  f2ndres  7856  mpomptsx  7904  dmmpossx  7906  fmpox  7907  ovmptss  7933  fparlem3  7954  fparlem4  7955  suppval  7979  suppsnop  7994  ressuppssdif  8001  brtpos2  8048  dftpos4  8061  tpostpos  8062  eceq1  8536  fvdiagfn  8679  mapsncnv  8681  elixpsn  8725  ixpsnf1o  8726  ensn1g  8809  en1  8811  en1OLD  8812  difsnen  8840  xpsneng  8843  xpcomco  8849  xpassen  8853  xpdom2  8854  canth2  8917  rexdif1en  8944  cnvfi  8963  phplem3OLD  9002  xpfi  9085  marypha2lem2  9195  cardsn  9727  pm54.43  9759  dfac5lem3  9881  dfac5lem4  9882  kmlem9  9914  kmlem11  9916  kmlem12  9917  ackbij1lem8  9983  r1om  10000  fictb  10001  hsmexlem4  10185  axcc2lem  10192  axcc2  10193  axdc3lem4  10209  fpwwe2cbv  10386  fpwwe2lem3  10389  fpwwecbv  10400  canth4  10403  s3iunsndisj  14679  fsum2dlem  15482  fsumcnv  15485  fsumcom2  15486  ackbijnn  15540  fprod2dlem  15690  fprodcnv  15693  fprodcom2  15694  lcmfunsnlem1  16342  lcmfunsnlem2lem1  16343  lcmfunsnlem2lem2  16344  lcmfunsnlem2  16345  lcmfunsn  16349  vdwlem1  16682  vdwlem12  16693  vdwlem13  16694  vdwnn  16699  0ram  16721  ramz2  16725  pwsval  17197  symg2bas  19000  symgfixelsi  19043  pmtrfv  19060  pmtrprfval  19095  sylow2a  19224  efgrelexlema  19355  gsum2dlem2  19572  gsum2d2  19575  gsumcom2  19576  dprdcntz  19611  dprddisj  19612  dprd2dlem2  19643  dprd2dlem1  19644  dprd2da  19645  ablfac1eu  19676  ablfaclem3  19690  lssats2  20262  lspsneq0  20274  lbsind  20342  lspsneq  20384  lspdisj2  20389  lspsnsubn0  20402  lspprat  20415  islbs2  20416  lbsextlem4  20423  lbsextg  20424  lpi0  20518  lpi1  20519  frlmlbs  21004  lindfind  21023  lindsind  21024  lindfrn  21028  psrvsca  21160  evlssca  21299  mpfind  21317  coe1fv  21377  coe1tm  21444  pf1ind  21521  submaval  21730  mdetunilem3  21763  mdetunilem4  21764  mdetunilem9  21769  islp  22291  perfi  22306  t1sncld  22477  bwth  22561  dis2ndc  22611  nllyi  22626  dissnlocfin  22680  ptbasfi  22732  txkgen  22803  xkofvcn  22835  xkoinjcn  22838  qtopeu  22867  txswaphmeolem  22955  pt1hmeo  22957  elflim2  23115  cnextfvval  23216  cnextcn  23218  cnextfres1  23219  cnextfres  23220  tsmsxplem1  23304  tsmsxplem2  23305  ucncn  23437  itg11  24855  i1faddlem  24857  i1fmullem  24858  itg1addlem3  24862  itg1mulc  24869  eldv  25062  ply1lpir  25343  areambl  26108  tglngval  26912  edglnl  27513  nbgrval  27703  nbgr2vtx1edg  27717  nbuhgr2vtx1edgb  27719  nbgr1vtx  27725  nb3grprlem2  27748  uvtxel  27755  uvtxel1  27763  uvtxusgrel  27770  cusgredg  27791  cplgr1v  27797  cplgr3v  27802  usgredgsscusgredg  27826  vtxdgval  27835  1loopgrvd2  27870  wlk1walk  28006  wlkres  28038  wlkp1lem8  28048  usgr2pthlem  28131  crctcshwlkn0lem6  28180  2wspiundisj  28328  clwwlknon1  28461  1wlkdlem4  28504  eupth2lem3lem3  28594  frcond1  28630  frgr1v  28635  nfrgr2v  28636  frgr3v  28639  1vwmgr  28640  3vfriswmgr  28642  3cyclfrgrrn1  28649  n4cyclfrgr  28655  frgrwopreglem4a  28674  h1de2ctlem  29917  spansn  29921  elspansn  29928  elspansn2  29929  spansneleq  29932  h1datom  29944  spansnj  30009  spansncv  30015  superpos  30716  sumdmdlem2  30781  aciunf1lem  30999  fnpreimac  31008  dfcnv2  31013  pwrssmgc  31278  gsummpt2co  31308  gsumpart  31315  0nellinds  31566  lindssn  31573  lsmsnidl  31587  nsgmgclem  31596  nsgmgc  31597  nsgqusf1olem1  31598  nsgqusf1olem2  31599  nsgqusf1olem3  31600  elrspunidl  31606  lbslsat  31699  lindsunlem  31705  extdgval  31729  locfinreflem  31790  esum2dlem  32060  sibfima  32305  sibfof  32307  bnj1373  33010  bnj1489  33036  funen1cnv  33060  fineqvac  33066  cplgredgex  33082  pfxwlk  33085  revwlk  33086  loop1cycl  33099  cvmscbv  33220  cvmsdisj  33232  cvmsss2  33236  cvmliftlem15  33260  cvmlift2lem11  33275  cvmlift2lem12  33276  cvmlift2lem13  33277  satffunlem1lem1  33364  satffunlem2lem1  33366  mvtinf  33517  eldm3  33728  elima4  33750  xpord2pred  33792  xpord3pred  33798  naddcllem  33831  conway  33993  scutval  33994  scutcut  33995  scutbday  33998  eqscut  33999  eqscut2  34000  scutun12  34004  scutbdaybnd  34009  scutbdaybnd2  34010  scutbdaylt  34012  bday1s  34025  madebdaylemlrcut  34079  cofcut1  34090  cofcutr  34092  fvsingle  34222  snelsingles  34224  dfiota3  34225  brapply  34240  funpartlem  34244  altopeq12  34264  ranksng  34469  neibastop3  34551  tailval  34562  filnetlem4  34570  bj-restsnss  35254  bj-restsnss2  35255  f1omptsnlem  35507  f1omptsn  35508  mptsnun  35510  dissneqlem  35511  dissneq  35512  fvineqsnf1  35581  lindsadd  35770  lindsenlbs  35772  poimirlem4  35781  poimirlem25  35802  poimirlem26  35803  poimirlem27  35804  poimirlem31  35808  poimirlem32  35809  heiborlem3  35971  ismrer1  35996  lshpnel2N  36999  lsatlspsn2  37006  lsatlspsn  37007  lsatspn0  37014  lkrscss  37112  lfl1dim  37135  lfl1dim2N  37136  ldualvs  37151  atpointN  37757  watvalN  38007  trnsetN  38170  dih1dimatlem  39343  dihatexv  39352  dihjat1lem  39442  dihjat1  39443  lcfl7N  39515  lcfl8  39516  lcfl9a  39519  lcfrlem8  39563  lcfrlem9  39564  lcf1o  39565  mapdval2N  39644  mapdval4N  39646  mapdspex  39682  mapdn0  39683  mapdpglem23  39708  mapdpg  39720  mapdindp1  39734  mapdheq  39742  hvmapval  39774  mapdh9a  39803  hdmap1eq  39815  hdmap1cbv  39816  hdmapval  39842  hdmap10  39854  hdmaplkr  39927  sn-iotalem  40189  sn-iotanul  40194  evlsbagval  40275  0prjspnrel  40464  mzpclval  40547  mzpcl1  40551  wopprc  40852  dnnumch3lem  40871  aomclem8  40886  mendvsca  41016  cytpval  41034  snen1g  41131  k0004lem3  41759  dvconstbi  41952  wessf1ornlem  42722  dvmptfprodlem  43485  fourierdlem32  43680  fourierdlem33  43681  fourierdlem48  43695  funressnmo  44540  aiotajust  44576  funressndmafv2rn  44715  fzopredsuc  44815  elsprel  44927  irinitoringc  45627  opeliun2xp  45668  dmmpossx2  45672  lindslinindsimp2  45804  ldepspr  45814  ldepsnlinc  45849  line  46078  rrxline  46080  setc2othin  46337  mndtcval  46366  mndtcbas  46368