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  6527  dftpos4  6539  tpostpos  6540  eceq1  6847  fvdiagfn  6981  mapsncnv  6983  elixpsn  7023  ixpsnf1o  7024  ensn1g  7090  en1  7092  xpsneng  7126  xpcomco  7130  xpassen  7134  xpdom2  7135  phplem3  7161  phplem3g  7163  fidifsnen  7178  xpfi  7245  isfsuppfi  7296  pm54.43  7542  cc2lem  7638  cc2  7639  exp3val  10998  fsum2dlemstep  12225  fsumcnv  12228  fisumcom2  12229  fprod2dlemstep  12413  fprodcnv  12416  fprodcom2fi  12417  gsum2dfilem2  14271  gsum2dfi  14272  gsum2d2fi  14273  gsumcom2fi  14274  pwsval  14310  lssats2  14859  lspsneq0  14871  txswaphmeolem  15563  vtxdgfifival  16754  vtxdumgrfival  16761  1loopgrvd2fi  16768  wlk1walkdom  16822  wlkres  16842  eupth2lem3lem3fi  16933