Theorem sneq 3648

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 2216	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2324	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 3643	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 3643	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2264	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1373  {cab 2192  {csn 3637

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-sn 3643

This theorem is referenced by:  sneqi  3649  sneqd  3650  euabsn  3707  absneu  3709  preq1  3714  tpeq3  3725  snssgOLD  3774  sneqrg  3808  sneqbg  3809  opeq1  3824  unisng  3872  exmidsssn  4253  exmidsssnc  4254  suceq  4456  snnex  4502  opeliunxp  4737  relop  4835  elimasng  5058  dmsnsnsng  5168  elxp4  5178  elxp5  5179  iotajust  5239  fconstg  5483  f1osng  5575  nfvres  5622  fsng  5765  funopsn  5774  fnressn  5782  fressnfv  5783  funfvima3  5830  isoselem  5901  1stvalg  6240  2ndvalg  6241  2ndval2  6254  fo1st  6255  fo2nd  6256  f1stres  6257  f2ndres  6258  mpomptsx  6295  dmmpossx  6297  fmpox  6298  brtpos2  6349  dftpos4  6361  tpostpos  6362  eceq1  6667  fvdiagfn  6792  mapsncnv  6794  elixpsn  6834  ixpsnf1o  6835  ensn1g  6901  en1  6903  xpsneng  6931  xpcomco  6935  xpassen  6939  xpdom2  6940  phplem3  6965  phplem3g  6967  fidifsnen  6981  xpfi  7043  pm54.43  7312  cc2lem  7393  cc2  7394  exp3val  10703  fsum2dlemstep  11815  fsumcnv  11818  fisumcom2  11819  fprod2dlemstep  12003  fprodcnv  12006  fprodcom2fi  12007  pwsval  13193  lssats2  14246  lspsneq0  14258  txswaphmeolem  14862