Theorem sneq 3587

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 2175	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2284	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 3582	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 3582	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2224	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1343  {cab 2151  {csn 3576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-sn 3582

This theorem is referenced by:  sneqi  3588  sneqd  3589  euabsn  3646  absneu  3648  preq1  3653  tpeq3  3664  snssg  3709  sneqrg  3742  sneqbg  3743  opeq1  3758  unisng  3806  exmidsssn  4181  exmidsssnc  4182  suceq  4380  snnex  4426  opeliunxp  4659  relop  4754  elimasng  4972  dmsnsnsng  5081  elxp4  5091  elxp5  5092  iotajust  5152  fconstg  5384  f1osng  5473  nfvres  5519  fsng  5658  fnressn  5671  fressnfv  5672  funfvima3  5718  isoselem  5788  1stvalg  6110  2ndvalg  6111  2ndval2  6124  fo1st  6125  fo2nd  6126  f1stres  6127  f2ndres  6128  mpomptsx  6165  dmmpossx  6167  fmpox  6168  brtpos2  6219  dftpos4  6231  tpostpos  6232  eceq1  6536  fvdiagfn  6659  mapsncnv  6661  elixpsn  6701  ixpsnf1o  6702  ensn1g  6763  en1  6765  xpsneng  6788  xpcomco  6792  xpassen  6796  xpdom2  6797  phplem3  6820  phplem3g  6822  fidifsnen  6836  xpfi  6895  pm54.43  7146  cc2lem  7207  cc2  7208  exp3val  10457  fsum2dlemstep  11375  fsumcnv  11378  fisumcom2  11379  fprod2dlemstep  11563  fprodcnv  11566  fprodcom2fi  11567  txswaphmeolem  12970