Theorem sneq 3720

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 2248	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2358	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 3715	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 3715	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2296	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

This proof depends on syntax axioms:   → wi 4   = wceq 1402  {cab 2224  {csn 3709

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-sn 3715

This theorem is used by:  sneqi  3721  sneqd  3722  euabsn  3781  absneu  3783  preq1  3788  tpeq3  3799  snssgOLD  3851  sneqrg  3887  sneqbg  3888  opeq1  3904  unisng  3952  exmidsssn  4341  exmidsssnc  4342  suceq  4549  snnex  4596  opeliunxp  4832  relop  4932  elimasng  5158  dmsnsnsng  5268  elxp4  5278  elxp5  5279  iotajust  5339  fconstg  5592  f1osng  5685  nfvres  5735  fsng  5884  fsn2g  5886  funopsn  5894  fnressn  5904  fressnfv  5905  funfvima3  5955  isoselem  6029  1stvalg  6380  2ndvalg  6381  2ndval2  6394  fo1st  6395  fo2nd  6396  f1stres  6397  f2ndres  6398  mpomptsx  6437  dmmpossx  6439  fmpox  6440  suppval  6481  suppsnopdc  6494  brtpos2  6526  dftpos4  6538  tpostpos  6539  eceq1  6846  fvdiagfn  6979  mapsncnv  6981  elixpsn  7021  ixpsnf1o  7022  ensn1g  7088  en1  7090  xpsneng  7124  xpcomco  7128  xpassen  7132  xpdom2  7133  phplem3  7159  phplem3g  7161  fidifsnen  7176  xpfi  7243  pm54.43  7542  cc2lem  7638  cc2  7639  exp3val  10999  fsum2dlemstep  12226  fsumcnv  12229  fisumcom2  12230  fprod2dlemstep  12414  fprodcnv  12417  fprodcom2fi  12418  gsum2dfilem2  14272  gsum2dfi  14273  gsum2d2fi  14274  gsumcom2fi  14275  pwsval  14311  lssats2  14860  lspsneq0  14872  txswaphmeolem  15546  vtxdgfifival  16737  vtxdumgrfival  16744  1loopgrvd2fi  16751  wlk1walkdom  16805  wlkres  16825  eupth2lem3lem3fi  16916