Theorem sneq 3677

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 2239	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2347	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 3672	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 3672	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2287	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1395  {cab 2215  {csn 3666

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-sn 3672

This theorem is referenced by:  sneqi  3678  sneqd  3679  euabsn  3736  absneu  3738  preq1  3743  tpeq3  3754  snssgOLD  3803  sneqrg  3839  sneqbg  3840  opeq1  3856  unisng  3904  exmidsssn  4285  exmidsssnc  4286  suceq  4492  snnex  4538  opeliunxp  4773  relop  4871  elimasng  5095  dmsnsnsng  5205  elxp4  5215  elxp5  5216  iotajust  5276  fconstg  5521  f1osng  5613  nfvres  5662  fsng  5807  funopsn  5816  fnressn  5824  fressnfv  5825  funfvima3  5872  isoselem  5943  1stvalg  6286  2ndvalg  6287  2ndval2  6300  fo1st  6301  fo2nd  6302  f1stres  6303  f2ndres  6304  mpomptsx  6341  dmmpossx  6343  fmpox  6344  brtpos2  6395  dftpos4  6407  tpostpos  6408  eceq1  6713  fvdiagfn  6838  mapsncnv  6840  elixpsn  6880  ixpsnf1o  6881  ensn1g  6947  en1  6949  xpsneng  6977  xpcomco  6981  xpassen  6985  xpdom2  6986  phplem3  7011  phplem3g  7013  fidifsnen  7028  xpfi  7090  pm54.43  7359  cc2lem  7448  cc2  7449  exp3val  10758  fsum2dlemstep  11940  fsumcnv  11943  fisumcom2  11944  fprod2dlemstep  12128  fprodcnv  12131  fprodcom2fi  12132  pwsval  13319  lssats2  14372  lspsneq0  14384  txswaphmeolem  14988