Theorem sneq 3680

Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
sneq	⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Proof of Theorem sneq

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq2 2241	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2349	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 3675	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 3675	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2289	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1397  {cab 2217  {csn 3669

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-sn 3675

This theorem is referenced by:  sneqi  3681  sneqd  3682  euabsn  3741  absneu  3743  preq1  3748  tpeq3  3759  snssgOLD  3809  sneqrg  3845  sneqbg  3846  opeq1  3862  unisng  3910  exmidsssn  4292  exmidsssnc  4293  suceq  4499  snnex  4545  opeliunxp  4781  relop  4880  elimasng  5104  dmsnsnsng  5214  elxp4  5224  elxp5  5225  iotajust  5285  fconstg  5533  f1osng  5626  nfvres  5675  fsng  5820  funopsn  5829  fnressn  5839  fressnfv  5840  funfvima3  5887  isoselem  5960  1stvalg  6304  2ndvalg  6305  2ndval2  6318  fo1st  6319  fo2nd  6320  f1stres  6321  f2ndres  6322  mpomptsx  6361  dmmpossx  6363  fmpox  6364  brtpos2  6416  dftpos4  6428  tpostpos  6429  eceq1  6736  fvdiagfn  6861  mapsncnv  6863  elixpsn  6903  ixpsnf1o  6904  ensn1g  6970  en1  6972  xpsneng  7005  xpcomco  7009  xpassen  7013  xpdom2  7014  phplem3  7039  phplem3g  7041  fidifsnen  7056  xpfi  7123  pm54.43  7394  cc2lem  7484  cc2  7485  exp3val  10802  fsum2dlemstep  11994  fsumcnv  11997  fisumcom2  11998  fprod2dlemstep  12182  fprodcnv  12185  fprodcom2fi  12186  pwsval  13373  lssats2  14427  lspsneq0  14439  txswaphmeolem  15043  vtxdgfifival  16141  vtxdumgrfival  16148  1loopgrvd2fi  16155  wlk1walkdom  16209  wlkres  16229