Theorem sneq 3655

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 2217	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2325	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 3650	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 3650	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2265	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1373  {cab 2193  {csn 3644

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-sn 3650

This theorem is referenced by:  sneqi  3656  sneqd  3657  euabsn  3714  absneu  3716  preq1  3721  tpeq3  3732  snssgOLD  3781  sneqrg  3817  sneqbg  3818  opeq1  3834  unisng  3882  exmidsssn  4263  exmidsssnc  4264  suceq  4468  snnex  4514  opeliunxp  4749  relop  4847  elimasng  5070  dmsnsnsng  5180  elxp4  5190  elxp5  5191  iotajust  5251  fconstg  5495  f1osng  5587  nfvres  5634  fsng  5778  funopsn  5787  fnressn  5795  fressnfv  5796  funfvima3  5843  isoselem  5914  1stvalg  6253  2ndvalg  6254  2ndval2  6267  fo1st  6268  fo2nd  6269  f1stres  6270  f2ndres  6271  mpomptsx  6308  dmmpossx  6310  fmpox  6311  brtpos2  6362  dftpos4  6374  tpostpos  6375  eceq1  6680  fvdiagfn  6805  mapsncnv  6807  elixpsn  6847  ixpsnf1o  6848  ensn1g  6914  en1  6916  xpsneng  6944  xpcomco  6948  xpassen  6952  xpdom2  6953  phplem3  6978  phplem3g  6980  fidifsnen  6995  xpfi  7057  pm54.43  7326  cc2lem  7415  cc2  7416  exp3val  10725  fsum2dlemstep  11906  fsumcnv  11909  fisumcom2  11910  fprod2dlemstep  12094  fprodcnv  12097  fprodcom2fi  12098  pwsval  13284  lssats2  14337  lspsneq0  14349  txswaphmeolem  14953