Theorem sneq 3605

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 2187	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2295	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 3600	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 3600	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2235	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1353  {cab 2163  {csn 3594

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-sn 3600

This theorem is referenced by:  sneqi  3606  sneqd  3607  euabsn  3664  absneu  3666  preq1  3671  tpeq3  3682  snssgOLD  3730  sneqrg  3764  sneqbg  3765  opeq1  3780  unisng  3828  exmidsssn  4204  exmidsssnc  4205  suceq  4404  snnex  4450  opeliunxp  4683  relop  4779  elimasng  4998  dmsnsnsng  5108  elxp4  5118  elxp5  5119  iotajust  5179  fconstg  5414  f1osng  5504  nfvres  5550  fsng  5691  fnressn  5704  fressnfv  5705  funfvima3  5752  isoselem  5823  1stvalg  6145  2ndvalg  6146  2ndval2  6159  fo1st  6160  fo2nd  6161  f1stres  6162  f2ndres  6163  mpomptsx  6200  dmmpossx  6202  fmpox  6203  brtpos2  6254  dftpos4  6266  tpostpos  6267  eceq1  6572  fvdiagfn  6695  mapsncnv  6697  elixpsn  6737  ixpsnf1o  6738  ensn1g  6799  en1  6801  xpsneng  6824  xpcomco  6828  xpassen  6832  xpdom2  6833  phplem3  6856  phplem3g  6858  fidifsnen  6872  xpfi  6931  pm54.43  7191  cc2lem  7267  cc2  7268  exp3val  10524  fsum2dlemstep  11444  fsumcnv  11447  fisumcom2  11448  fprod2dlemstep  11632  fprodcnv  11635  fprodcom2fi  11636  txswaphmeolem  13859