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  fsn2g  5822  funopsn  5830  fnressn  5840  fressnfv  5841  funfvima3  5888  isoselem  5961  1stvalg  6305  2ndvalg  6306  2ndval2  6319  fo1st  6320  fo2nd  6321  f1stres  6322  f2ndres  6323  mpomptsx  6362  dmmpossx  6364  fmpox  6365  brtpos2  6417  dftpos4  6429  tpostpos  6430  eceq1  6737  fvdiagfn  6862  mapsncnv  6864  elixpsn  6904  ixpsnf1o  6905  ensn1g  6971  en1  6973  xpsneng  7006  xpcomco  7010  xpassen  7014  xpdom2  7015  phplem3  7040  phplem3g  7042  fidifsnen  7057  xpfi  7124  pm54.43  7395  cc2lem  7485  cc2  7486  exp3val  10804  fsum2dlemstep  12000  fsumcnv  12003  fisumcom2  12004  fprod2dlemstep  12188  fprodcnv  12191  fprodcom2fi  12192  pwsval  13379  lssats2  14434  lspsneq0  14446  txswaphmeolem  15050  vtxdgfifival  16148  vtxdumgrfival  16155  1loopgrvd2fi  16162  wlk1walkdom  16216  wlkres  16236  eupth2lem3lem3fi  16327