Theorem sneq 3678

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 2239	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2347	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 3673	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 3673	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2287	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1395  {cab 2215  {csn 3667

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-sn 3673

This theorem is referenced by:  sneqi  3679  sneqd  3680  euabsn  3739  absneu  3741  preq1  3746  tpeq3  3757  snssgOLD  3807  sneqrg  3843  sneqbg  3844  opeq1  3860  unisng  3908  exmidsssn  4290  exmidsssnc  4291  suceq  4497  snnex  4543  opeliunxp  4779  relop  4878  elimasng  5102  dmsnsnsng  5212  elxp4  5222  elxp5  5223  iotajust  5283  fconstg  5530  f1osng  5622  nfvres  5671  fsng  5816  funopsn  5825  fnressn  5835  fressnfv  5836  funfvima3  5883  isoselem  5956  1stvalg  6300  2ndvalg  6301  2ndval2  6314  fo1st  6315  fo2nd  6316  f1stres  6317  f2ndres  6318  mpomptsx  6357  dmmpossx  6359  fmpox  6360  brtpos2  6412  dftpos4  6424  tpostpos  6425  eceq1  6732  fvdiagfn  6857  mapsncnv  6859  elixpsn  6899  ixpsnf1o  6900  ensn1g  6966  en1  6968  xpsneng  7001  xpcomco  7005  xpassen  7009  xpdom2  7010  phplem3  7035  phplem3g  7037  fidifsnen  7052  xpfi  7117  pm54.43  7386  cc2lem  7475  cc2  7476  exp3val  10793  fsum2dlemstep  11985  fsumcnv  11988  fisumcom2  11989  fprod2dlemstep  12173  fprodcnv  12176  fprodcom2fi  12177  pwsval  13364  lssats2  14418  lspsneq0  14430  txswaphmeolem  15034  vtxdgfifival  16097  vtxdumgrfival  16104  1loopgrvd2fi  16111  wlk1walkdom  16156  wlkres  16174