Theorem sneq 3386

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 2049	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2155	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 3381	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 3381	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2097	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1243  {cab 2026  {csn 3375

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-sn 3381

This theorem is referenced by:  sneqi  3387  sneqd  3388  euabsn  3440  absneu  3442  preq1  3447  tpeq3  3458  snssg  3500  sneqrg  3533  sneqbg  3534  opeq1  3549  unisng  3597  suceq  4139  snnex  4181  opeliunxp  4395  relop  4486  elimasng  4693  dmsnsnsng  4798  elxp4  4808  elxp5  4809  iotajust  4866  fconstg  5083  f1osng  5167  nfvres  5206  fsng  5336  fnressn  5349  fressnfv  5350  funfvima3  5392  isoselem  5459  1stvalg  5769  2ndvalg  5770  2ndval2  5783  fo1st  5784  fo2nd  5785  f1stres  5786  f2ndres  5787  mpt2mptsx  5823  dmmpt2ssx  5825  fmpt2x  5826  brtpos2  5866  dftpos4  5878  tpostpos  5879  eceq1  6141  ensn1g  6277  en1  6279  xpsneng  6296  xpcomco  6300  xpassen  6304  xpdom2  6305  phplem3  6317  phplem3g  6319  fidifsnen  6331  expival  9257