Theorem sneq 3594

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 2180	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2288	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 3589	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 3589	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2228	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1348  {cab 2156  {csn 3583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-sn 3589

This theorem is referenced by:  sneqi  3595  sneqd  3596  euabsn  3653  absneu  3655  preq1  3660  tpeq3  3671  snssg  3716  sneqrg  3749  sneqbg  3750  opeq1  3765  unisng  3813  exmidsssn  4188  exmidsssnc  4189  suceq  4387  snnex  4433  opeliunxp  4666  relop  4761  elimasng  4979  dmsnsnsng  5088  elxp4  5098  elxp5  5099  iotajust  5159  fconstg  5394  f1osng  5483  nfvres  5529  fsng  5669  fnressn  5682  fressnfv  5683  funfvima3  5729  isoselem  5799  1stvalg  6121  2ndvalg  6122  2ndval2  6135  fo1st  6136  fo2nd  6137  f1stres  6138  f2ndres  6139  mpomptsx  6176  dmmpossx  6178  fmpox  6179  brtpos2  6230  dftpos4  6242  tpostpos  6243  eceq1  6548  fvdiagfn  6671  mapsncnv  6673  elixpsn  6713  ixpsnf1o  6714  ensn1g  6775  en1  6777  xpsneng  6800  xpcomco  6804  xpassen  6808  xpdom2  6809  phplem3  6832  phplem3g  6834  fidifsnen  6848  xpfi  6907  pm54.43  7167  cc2lem  7228  cc2  7229  exp3val  10478  fsum2dlemstep  11397  fsumcnv  11400  fisumcom2  11401  fprod2dlemstep  11585  fprodcnv  11588  fprodcom2fi  11589  txswaphmeolem  13114