Theorem sneq 3502

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 2122	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2230	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 3497	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 3497	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2170	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1312  {cab 2099  {csn 3491

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-11 1465  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-sn 3497

This theorem is referenced by:  sneqi  3503  sneqd  3504  euabsn  3557  absneu  3559  preq1  3564  tpeq3  3575  snssg  3620  sneqrg  3653  sneqbg  3654  opeq1  3669  unisng  3717  exmidsssn  4083  exmidsssnc  4084  suceq  4282  snnex  4327  opeliunxp  4552  relop  4647  elimasng  4863  dmsnsnsng  4972  elxp4  4982  elxp5  4983  iotajust  5043  fconstg  5275  f1osng  5362  nfvres  5406  fsng  5545  fnressn  5558  fressnfv  5559  funfvima3  5603  isoselem  5673  1stvalg  5992  2ndvalg  5993  2ndval2  6006  fo1st  6007  fo2nd  6008  f1stres  6009  f2ndres  6010  mpomptsx  6047  dmmpossx  6049  fmpox  6050  brtpos2  6100  dftpos4  6112  tpostpos  6113  eceq1  6416  fvdiagfn  6539  mapsncnv  6541  elixpsn  6581  ixpsnf1o  6582  ensn1g  6643  en1  6645  xpsneng  6667  xpcomco  6671  xpassen  6675  xpdom2  6676  phplem3  6699  phplem3g  6701  fidifsnen  6715  xpfi  6769  pm54.43  6993  exp3val  10182  fsum2dlemstep  11089  fsumcnv  11092  fisumcom2  11093