Theorem sneq 3634

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 2206	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2314	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 3629	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 3629	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2254	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1364  {cab 2182  {csn 3623

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-sn 3629

This theorem is referenced by:  sneqi  3635  sneqd  3636  euabsn  3693  absneu  3695  preq1  3700  tpeq3  3711  snssgOLD  3759  sneqrg  3793  sneqbg  3794  opeq1  3809  unisng  3857  exmidsssn  4236  exmidsssnc  4237  suceq  4438  snnex  4484  opeliunxp  4719  relop  4817  elimasng  5038  dmsnsnsng  5148  elxp4  5158  elxp5  5159  iotajust  5219  fconstg  5457  f1osng  5548  nfvres  5595  fsng  5738  fnressn  5751  fressnfv  5752  funfvima3  5799  isoselem  5870  1stvalg  6209  2ndvalg  6210  2ndval2  6223  fo1st  6224  fo2nd  6225  f1stres  6226  f2ndres  6227  mpomptsx  6264  dmmpossx  6266  fmpox  6267  brtpos2  6318  dftpos4  6330  tpostpos  6331  eceq1  6636  fvdiagfn  6761  mapsncnv  6763  elixpsn  6803  ixpsnf1o  6804  ensn1g  6865  en1  6867  xpsneng  6890  xpcomco  6894  xpassen  6898  xpdom2  6899  phplem3  6924  phplem3g  6926  fidifsnen  6940  xpfi  7002  pm54.43  7269  cc2lem  7349  cc2  7350  exp3val  10650  fsum2dlemstep  11616  fsumcnv  11619  fisumcom2  11620  fprod2dlemstep  11804  fprodcnv  11807  fprodcom2fi  11808  pwsval  12993  lssats2  14046  lspsneq0  14058  txswaphmeolem  14640