Theorem sneq 4601

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 2777	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2831	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4592	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4592	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2825	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-sn 4592

This theorem is used by:  sneqi  4602  sneqd  4603  euabsn  4694  absneu  4696  preq1  4701  tpeq3  4712  issn  4799  mosneq  4809  sneqbg  4810  opeq1  4840  snexgALT  5414  propeqop  5492  opthwiener  5499  otiunsndisj  5505  opeliunxp  5730  opeliun2xp  5731  relop  5838  inisegn0  6102  xpdifid  6167  xpdifcnvepel  6168  dmsnsnsn  6223  predeq123  6307  iotajust  6495  iotanul2  6513  fconstg  6769  f1osng  6867  opabiotafun  6965  fvn0ssdmfun  7073  fsng  7137  fsn2g  7138  fnressn  7159  fressnfv  7161  funfvima3  7238  f12dfv  7277  f13dfv  7278  isofrlem  7344  isoselem  7345  elxp4  7921  elxp5  7922  1stval  7990  2ndval  7991  2ndval2  8006  fo1st  8008  fo2nd  8009  f1stres  8012  f2ndres  8013  mpomptsx  8063  dmmpossx  8065  fmpox  8066  ovmptss  8090  fparlem3  8111  fparlem4  8112  xpord2pred  8143  xpord3pred  8150  suppval  8160  suppsnop  8176  ressuppssdif  8183  brtpos2  8230  dftpos4  8243  tpostpos  8244  naddcllem  8664  eceq1  8736  fvdiagfn  8891  mapsncnv  8893  elixpsn  8937  ixpsnf1o  8938  ensn1g  9021  en1  9023  funen1cnv  9028  difsnen  9050  xpsneng  9053  xpcomco  9058  xpassen  9062  xpdom2  9063  canth2  9121  rexdif1en  9148  cnvfi  9163  marypha2lem2  9399  cardsn  9967  pm54.43  9999  dfac5lem3  10121  dfac5lem4  10122  kmlem9  10154  kmlem11  10156  kmlem12  10157  ackbij1lem8  10221  r1om  10238  fictb  10239  hsmexlem4  10424  axcc2lem  10431  axcc2  10432  axdc3lem4  10448  fpwwe2cbv  10626  fpwwe2lem3  10629  fpwwecbv  10640  canth4  10643  s3iunsndisj  15025  fsum2dlem  15840  fsumcnv  15843  fsumcom2  15844  ackbijnn  15901  fprod2dlem  16053  fprodcnv  16056  fprodcom2  16057  lcmfunsnlem1  16713  lcmfunsnlem2lem1  16714  lcmfunsnlem2lem2  16715  lcmfunsnlem2  16716  lcmfunsn  16720  vdwlem1  17059  vdwlem12  17070  vdwlem13  17071  vdwnn  17076  0ram  17098  ramz2  17102  pwsval  17557  symg2bas  19487  symgfixelsi  19529  pmtrfv  19546  pmtrprfval  19581  sylow2a  19713  efgrelexlema  19843  gsum2dlem2  20065  gsum2d2  20068  gsumcom2  20069  dprdcntz  20104  dprddisj  20105  dprd2dlem2  20136  dprd2dlem1  20137  dprd2da  20138  ablfac1eu  20169  ablfaclem3  20183  lssats2  21151  lspsneq0  21163  lbsind  21231  lspsneq  21276  lspdisj2  21281  lspsnsubn0  21294  lspprat  21307  islbs2  21308  lbsextlem4  21315  lbsextg  21316  lpi0  21524  lpi1  21525  irinitoringc  21659  pzriprnglem13  21673  pzriprnglem14  21674  frlmlbs  21977  lindfind  21996  lindsind  21997  lindfrn  22001  psrvsca  22129  evlsvvval  22274  evlssca  22275  mpfind  22296  evlsevl  22313  coe1fv  22396  coe1tm  22464  pf1ind  22545  submaval  22768  mdetunilem3  22801  mdetunilem4  22802  mdetunilem9  22807  islp  23327  perfi  23342  t1sncld  23513  bwth  23597  dis2ndc  23648  nllyi  23663  dissnlocfin  23717  ptbasfi  23769  txkgen  23840  xkofvcn  23872  xkoinjcn  23875  qtopeu  23904  txswaphmeolem  23992  pt1hmeo  23994  elflim2  24152  cnextfvval  24253  cnextcn  24255  cnextfres1  24256  cnextfres  24257  tsmsxplem1  24341  tsmsxplem2  24342  ucncn  24472  itg11  25881  i1faddlem  25883  i1fmullem  25884  itg1addlem3  25888  itg1mulc  25894  eldv  26088  ply1lpir  26370  areambl  27154  conway  28003  cutsval  28004  cutcuts  28005  cutbday  28008  eqcuts  28009  eqcuts2  28010  cutsun12  28014  cutbdaybnd  28019  cutbdaybnd2  28020  cutbdaylt  28022  eqcuts3  28028  bday1  28038  cuteq0  28039  cuteq1  28041  madebdaylemlrcut  28123  sltsbday  28141  cofcut1  28144  cofcutr  28148  oniso  28495  bdayn0p1  28593  expsval  28649  pw2cut2  28686  tglngval  28851  edglnl  29524  nbgrval  29720  nbgr2vtx1edg  29734  nbuhgr2vtx1edgb  29736  nbgr1vtx  29742  nb3grprlem2  29765  uvtxel  29772  uvtxel1  29780  uvtxusgrel  29787  cusgredg  29808  cplgr1v  29814  cplgr3v  29819  usgredgsscusgredg  29843  vtxdgval  29852  1loopgrvd2  29887  wlk1walk  30022  wlkres  30052  wlkp1lem8  30062  pfxwlk  30069  revwlk  30070  usgr2pthlem  30152  crctcshwlkn0lem6  30207  2wspiundisj  30358  clwwlknon1  30491  1wlkdlem4  30534  loop1cycl  30547  eupth2lem3lem3  30628  frcond1  30664  frgr1v  30669  nfrgr2v  30670  frgr3v  30673  1vwmgr  30674  3vfriswmgr  30676  3cyclfrgrrn1  30683  n4cyclfrgr  30689  frgrwopreglem4a  30708  h1de2ctlem  31954  spansn  31958  elspansn  31965  elspansn2  31966  spansneleq  31969  h1datom  31981  spansnj  32046  spansncv  32052  superpos  32753  sumdmdlem2  32818  aciunf1lem  33054  fnpreimac  33062  dfcnv2  33067  pwrssmgc  33360  gsummpt2co  33408  gsumpart  33423  gsumwrd2dccatlem  33437  gsumwrd2dccat  33438  0nellinds  33725  lindssn  33731  lsmsnidl  33750  nsgmgclem  33760  nsgmgc  33761  nsgqusf1olem1  33762  nsgqusf1olem2  33763  nsgqusf1olem3  33764  pidlnzb  33770  elrspunidl  33776  extvfval  33962  esplyfval1  34003  esplyfvaln  34004  lbslsat  34046  lindsunlem  34054  extdgval  34083  fldextrspunlsplem  34103  locfinreflem  34270  esum2dlem  34522  sibfima  34769  sibfof  34771  bnj1373  35459  bnj1489  35485  fineqvac  35562  onvfowev  35633  cplgredgex  35639  cvmscbv  35763  cvmsdisj  35775  cvmsss2  35779  cvmliftlem15  35803  cvmlift2lem11  35818  cvmlift2lem12  35819  cvmlift2lem13  35820  satffunlem1lem1  35907  satffunlem2lem1  35909  mvtinf  36060  eldm3  36266  elima4  36281  fvsingle  36423  snelsingles  36425  dfiota3  36426  brapply  36441  funpartlem  36447  altopeq12  36467  ranksng  36672  neibastop3  36906  tailval  36917  filnetlem4  36925  ttcid  37036  mh-inf3sn  37086  mh-infprim2bi  37091  mh-infprim3bi  37092  bj-snexg  37703  bj-restsnss  37758  bj-restsnss2  37759  f1omptsnlem  38015  f1omptsn  38016  mptsnun  38018  dissneqlem  38019  dissneq  38020  fvineqsnf1  38089  lindsadd  38297  lindsenlbs  38299  poimirlem4  38308  poimirlem25  38329  poimirlem26  38330  poimirlem27  38331  poimirlem31  38335  poimirlem32  38336  heiborlem3  38497  ismrer1  38522  lshpnel2N  39792  lsatlspsn2  39799  lsatlspsn  39800  lsatspn0  39807  lkrscss  39905  lfl1dim  39928  lfl1dim2N  39929  ldualvs  39944  atpointN  40550  watvalN  40800  trnsetN  40963  dih1dimatlem  42136  dihatexv  42145  dihjat1lem  42235  dihjat1  42236  lcfl7N  42308  lcfl8  42309  lcfl9a  42312  lcfrlem8  42356  lcfrlem9  42357  lcf1o  42358  mapdval2N  42437  mapdval4N  42439  mapdspex  42475  mapdn0  42476  mapdpglem23  42501  mapdpg  42513  mapdindp1  42527  mapdheq  42535  hvmapval  42567  mapdh9a  42596  hdmap1eq  42608  hdmap1cbv  42609  hdmapval  42635  hdmap10  42647  hdmaplkr  42720  sn-iotalem  43025  0prjspnrel  43392  mzpclval  43489  mzpcl1  43493  wopprc  43790  dnnumch3lem  43806  aomclem8  43821  mendvsca  43947  cytpval  43962  snen1g  44283  k0004lem3  44908  dvconstbi  45077  relpfrlem  45695  permaxinf2lem  45754  wessf1ornlem  45936  dvmptfprodlem  46691  fourierdlem32  46886  fourierdlem33  46887  fourierdlem48  46901  funressnmo  47816  aiotajust  47854  funressndmafv2rn  47993  fzopredsuc  48094  elsprel  48257  clnbgrval  48620  dfvopnbgr2  48651  vopnbgrel  48652  dfclnbgr6  48654  dfnbgr6  48655  cycl3grtri  48745  dmmpossx2  49150  lindslinindsimp2  49276  ldepspr  49286  ldepsnlinc  49321  line  49545  rrxline  49547  dftpos5  49685  tposideq  49699  initc  49902  setc2othin  50277  functermceu  50321  idfudiag1  50336  funcsn  50352  0fucterm  50354  mndtcval  50390  mndtcbas  50392