Theorem sneq 3409

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 2090	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2196	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 3404	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 3404	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2138	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1284  {cab 2067  {csn 3398

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-11 1437  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-sn 3404

This theorem is referenced by:  sneqi  3410  sneqd  3411  euabsn  3462  absneu  3464  preq1  3469  tpeq3  3480  snssg  3522  sneqrg  3554  sneqbg  3555  opeq1  3570  unisng  3618  suceq  4157  snnex  4199  opeliunxp  4413  relop  4504  elimasng  4713  dmsnsnsng  4818  elxp4  4828  elxp5  4829  iotajust  4886  fconstg  5103  f1osng  5187  nfvres  5227  fsng  5357  fnressn  5370  fressnfv  5371  funfvima3  5413  isoselem  5479  1stvalg  5789  2ndvalg  5790  2ndval2  5803  fo1st  5804  fo2nd  5805  f1stres  5806  f2ndres  5807  mpt2mptsx  5843  dmmpt2ssx  5845  fmpt2x  5846  brtpos2  5889  dftpos4  5901  tpostpos  5902  eceq1  6164  ensn1g  6300  en1  6302  xpsneng  6319  xpcomco  6323  xpassen  6327  xpdom2  6328  phplem3  6340  phplem3g  6342  fidifsnen  6355  pm54.43  6459  expival  9478