Theorem sneq 3618

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 2199	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2307	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 3613	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 3613	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2247	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1364  {cab 2175  {csn 3607

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-sn 3613

This theorem is referenced by:  sneqi  3619  sneqd  3620  euabsn  3677  absneu  3679  preq1  3684  tpeq3  3695  snssgOLD  3743  sneqrg  3777  sneqbg  3778  opeq1  3793  unisng  3841  exmidsssn  4220  exmidsssnc  4221  suceq  4420  snnex  4466  opeliunxp  4699  relop  4795  elimasng  5014  dmsnsnsng  5124  elxp4  5134  elxp5  5135  iotajust  5195  fconstg  5431  f1osng  5521  nfvres  5568  fsng  5710  fnressn  5723  fressnfv  5724  funfvima3  5771  isoselem  5842  1stvalg  6168  2ndvalg  6169  2ndval2  6182  fo1st  6183  fo2nd  6184  f1stres  6185  f2ndres  6186  mpomptsx  6223  dmmpossx  6225  fmpox  6226  brtpos2  6277  dftpos4  6289  tpostpos  6290  eceq1  6595  fvdiagfn  6720  mapsncnv  6722  elixpsn  6762  ixpsnf1o  6763  ensn1g  6824  en1  6826  xpsneng  6849  xpcomco  6853  xpassen  6857  xpdom2  6858  phplem3  6883  phplem3g  6885  fidifsnen  6899  xpfi  6959  pm54.43  7220  cc2lem  7296  cc2  7297  exp3val  10556  fsum2dlemstep  11477  fsumcnv  11480  fisumcom2  11481  fprod2dlemstep  11665  fprodcnv  11668  fprodcom2fi  11669  lssats2  13747  lspsneq0  13759  txswaphmeolem  14297