Theorem sneqd 3632

Description: Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.)

Hypothesis

Ref	Expression
sneqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sneqd	⊢ (𝜑 → {𝐴} = {𝐵})

Proof of Theorem sneqd

Step	Hyp	Ref	Expression
1		sneqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sneq 3630	. 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	syl 14	1 ⊢ (𝜑 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1364  {csn 3619

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 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-sn 3625

This theorem is referenced by:  dmsnsnsng  5144  cnvsng  5152  ressn  5207  f1osng  5542  fsng  5732  fnressn  5745  fvsng  5755  2nd1st  6235  dfmpo  6278  cnvf1olem  6279  tpostpos  6319  tfrlemi1  6387  tfr1onlemaccex  6403  tfrcllemaccex  6416  elixpsn  6791  ixpsnf1o  6792  en1bg  6856  mapsnen  6867  xpassen  6886  fztp  10147  fzsuc2  10148  fseq1p1m1  10163  fseq1m1p1  10164  zfz1isolemsplit  10912  zfz1isolem1  10914  fsumm1  11562  fprodm1  11744  divalgmod  12071  ennnfonelemg  12563  ennnfonelemp1  12566  ennnfonelem1  12567  ennnfonelemnn0  12582  setsvalg  12651  strsetsid  12654  imasex  12891  imasival  12892  imasaddvallemg  12901  mulgval  13195  isunitd  13605  lspsnneg  13919  lspsnsub  13920  lmodindp1  13927  lidl0  13988  rsp0  13992  ridl0  14009  zrhrhmb  14121  znval  14135  psrval  14163  txdis  14456