Theorem sneq 4599

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 2741	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2795	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4590	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4590	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1540  {cab 2707  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-sn 4590

This theorem is referenced by:  sneqi  4600  sneqd  4601  euabsn  4690  absneu  4692  preq1  4697  tpeq3  4708  issn  4796  mosneq  4806  sneqbg  4807  opeq1  4837  snexg  5390  propeqop  5467  opthwiener  5474  otiunsndisj  5480  opeliunxp  5705  opeliun2xp  5706  relop  5814  inisegn0  6069  xpdifid  6141  dmsnsnsn  6193  predeq123  6275  iotajust  6463  iotanul2  6481  fconstg  6747  f1osng  6841  opabiotafun  6941  fvn0ssdmfun  7046  fsng  7109  fsn2g  7110  fnressn  7130  fressnfv  7132  funfvima3  7210  f12dfv  7248  f13dfv  7249  isofrlem  7315  isoselem  7316  elxp4  7898  elxp5  7899  1stval  7970  2ndval  7971  2ndval2  7986  fo1st  7988  fo2nd  7989  f1stres  7992  f2ndres  7993  mpomptsx  8043  dmmpossx  8045  fmpox  8046  ovmptss  8072  fparlem3  8093  fparlem4  8094  xpord2pred  8124  xpord3pred  8131  suppval  8141  suppsnop  8157  ressuppssdif  8164  brtpos2  8211  dftpos4  8224  tpostpos  8225  naddcllem  8640  eceq1  8710  fvdiagfn  8864  mapsncnv  8866  elixpsn  8910  ixpsnf1o  8911  ensn1g  8993  en1  8995  difsnen  9023  xpsneng  9026  xpcomco  9031  xpassen  9035  xpdom2  9036  canth2  9094  rexdif1en  9122  rexdif1enOLD  9123  cnvfi  9140  xpfiOLD  9270  marypha2lem2  9387  cardsn  9922  pm54.43  9954  dfac5lem3  10078  dfac5lem4  10079  dfac5lem4OLD  10081  kmlem9  10112  kmlem11  10114  kmlem12  10115  ackbij1lem8  10179  r1om  10196  fictb  10197  hsmexlem4  10382  axcc2lem  10389  axcc2  10390  axdc3lem4  10406  fpwwe2cbv  10583  fpwwe2lem3  10586  fpwwecbv  10597  canth4  10600  s3iunsndisj  14934  fsum2dlem  15736  fsumcnv  15739  fsumcom2  15740  ackbijnn  15794  fprod2dlem  15946  fprodcnv  15949  fprodcom2  15950  lcmfunsnlem1  16607  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  lcmfunsnlem2  16610  lcmfunsn  16614  vdwlem1  16952  vdwlem12  16963  vdwlem13  16964  vdwnn  16969  0ram  16991  ramz2  16995  pwsval  17449  symg2bas  19323  symgfixelsi  19365  pmtrfv  19382  pmtrprfval  19417  sylow2a  19549  efgrelexlema  19679  gsum2dlem2  19901  gsum2d2  19904  gsumcom2  19905  dprdcntz  19940  dprddisj  19941  dprd2dlem2  19972  dprd2dlem1  19973  dprd2da  19974  ablfac1eu  20005  ablfaclem3  20019  lssats2  20906  lspsneq0  20918  lbsind  20987  lspsneq  21032  lspdisj2  21037  lspsnsubn0  21050  lspprat  21063  islbs2  21064  lbsextlem4  21071  lbsextg  21072  lpi0  21236  lpi1  21237  irinitoringc  21389  pzriprnglem13  21403  pzriprnglem14  21404  frlmlbs  21706  lindfind  21725  lindsind  21726  lindfrn  21730  psrvsca  21858  evlssca  21996  mpfind  22014  coe1fv  22091  coe1tm  22159  pf1ind  22242  submaval  22468  mdetunilem3  22501  mdetunilem4  22502  mdetunilem9  22507  islp  23027  perfi  23042  t1sncld  23213  bwth  23297  dis2ndc  23347  nllyi  23362  dissnlocfin  23416  ptbasfi  23468  txkgen  23539  xkofvcn  23571  xkoinjcn  23574  qtopeu  23603  txswaphmeolem  23691  pt1hmeo  23693  elflim2  23851  cnextfvval  23952  cnextcn  23954  cnextfres1  23955  cnextfres  23956  tsmsxplem1  24040  tsmsxplem2  24041  ucncn  24172  itg11  25592  i1faddlem  25594  i1fmullem  25595  itg1addlem3  25599  itg1mulc  25605  eldv  25799  ply1lpir  26087  areambl  26868  conway  27711  scutval  27712  scutcut  27713  scutbday  27716  eqscut  27717  eqscut2  27718  scutun12  27722  scutbdaybnd  27727  scutbdaybnd2  27728  scutbdaylt  27730  bday1s  27743  cuteq0  27744  cuteq1  27746  madebdaylemlrcut  27810  cofcut1  27828  cofcutr  27832  onsiso  28169  bdayn0p1  28258  expsval  28311  tglngval  28478  edglnl  29070  nbgrval  29263  nbgr2vtx1edg  29277  nbuhgr2vtx1edgb  29279  nbgr1vtx  29285  nb3grprlem2  29308  uvtxel  29315  uvtxel1  29323  uvtxusgrel  29330  cusgredg  29351  cplgr1v  29357  cplgr3v  29362  usgredgsscusgredg  29387  vtxdgval  29396  1loopgrvd2  29431  wlk1walk  29567  wlkres  29598  wlkp1lem8  29608  usgr2pthlem  29693  crctcshwlkn0lem6  29745  2wspiundisj  29893  clwwlknon1  30026  1wlkdlem4  30069  eupth2lem3lem3  30159  frcond1  30195  frgr1v  30200  nfrgr2v  30201  frgr3v  30204  1vwmgr  30205  3vfriswmgr  30207  3cyclfrgrrn1  30214  n4cyclfrgr  30220  frgrwopreglem4a  30239  h1de2ctlem  31484  spansn  31488  elspansn  31495  elspansn2  31496  spansneleq  31499  h1datom  31511  spansnj  31576  spansncv  31582  superpos  32283  sumdmdlem2  32348  aciunf1lem  32586  fnpreimac  32595  dfcnv2  32600  pwrssmgc  32926  gsummpt2co  32988  gsumpart  32997  gsumwrd2dccatlem  33006  gsumwrd2dccat  33007  0nellinds  33341  lindssn  33349  lsmsnidl  33370  nsgmgclem  33382  nsgmgc  33383  nsgqusf1olem1  33384  nsgqusf1olem2  33385  nsgqusf1olem3  33386  pidlnzb  33393  elrspunidl  33399  lbslsat  33612  lindsunlem  33620  extdgval  33649  fldextrspunlsplem  33668  locfinreflem  33830  esum2dlem  34082  sibfima  34329  sibfof  34331  bnj1373  35020  bnj1489  35046  funen1cnv  35078  fineqvac  35087  cplgredgex  35108  pfxwlk  35111  revwlk  35112  loop1cycl  35124  cvmscbv  35245  cvmsdisj  35257  cvmsss2  35261  cvmliftlem15  35285  cvmlift2lem11  35300  cvmlift2lem12  35301  cvmlift2lem13  35302  satffunlem1lem1  35389  satffunlem2lem1  35391  mvtinf  35542  eldm3  35748  elima4  35763  fvsingle  35908  snelsingles  35910  dfiota3  35911  brapply  35926  funpartlem  35930  altopeq12  35950  ranksng  36155  neibastop3  36350  tailval  36361  filnetlem4  36369  bj-snexg  37022  bj-restsnss  37071  bj-restsnss2  37072  f1omptsnlem  37324  f1omptsn  37325  mptsnun  37327  dissneqlem  37328  dissneq  37329  fvineqsnf1  37398  lindsadd  37607  lindsenlbs  37609  poimirlem4  37618  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem31  37645  poimirlem32  37646  heiborlem3  37807  ismrer1  37832  lshpnel2N  38978  lsatlspsn2  38985  lsatlspsn  38986  lsatspn0  38993  lkrscss  39091  lfl1dim  39114  lfl1dim2N  39115  ldualvs  39130  atpointN  39737  watvalN  39987  trnsetN  40150  dih1dimatlem  41323  dihatexv  41332  dihjat1lem  41422  dihjat1  41423  lcfl7N  41495  lcfl8  41496  lcfl9a  41499  lcfrlem8  41543  lcfrlem9  41544  lcf1o  41545  mapdval2N  41624  mapdval4N  41626  mapdspex  41662  mapdn0  41663  mapdpglem23  41688  mapdpg  41700  mapdindp1  41714  mapdheq  41722  hvmapval  41754  mapdh9a  41783  hdmap1eq  41795  hdmap1cbv  41796  hdmapval  41822  hdmap10  41834  hdmaplkr  41907  sn-iotalem  42209  evlsvvval  42551  evlsevl  42559  0prjspnrel  42615  mzpclval  42713  mzpcl1  42717  wopprc  43019  dnnumch3lem  43035  aomclem8  43050  mendvsca  43176  cytpval  43191  snen1g  43513  k0004lem3  44138  dvconstbi  44323  relpfrlem  44943  permaxinf2lem  45002  wessf1ornlem  45179  dvmptfprodlem  45942  fourierdlem32  46137  fourierdlem33  46138  fourierdlem48  46152  funressnmo  47047  aiotajust  47085  funressndmafv2rn  47224  fzopredsuc  47324  elsprel  47476  clnbgrval  47823  dfvopnbgr2  47853  vopnbgrel  47854  dfclnbgr6  47856  dfnbgr6  47857  cycl3grtri  47946  dmmpossx2  48325  lindslinindsimp2  48452  ldepspr  48462  ldepsnlinc  48497  line  48721  rrxline  48723  dftpos5  48862  tposideq  48876  initc  49080  setc2othin  49455  functermceu  49499  idfudiag1  49514  funcsn  49530  0fucterm  49532  mndtcval  49568  mndtcbas  49570