Theorem sneqd 3506

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 3504	. 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	syl 14	1 ⊢ (𝜑 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1314  {csn 3493

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-sn 3499

This theorem is referenced by:  dmsnsnsng  4974  cnvsng  4982  ressn  5037  f1osng  5364  fsng  5547  fnressn  5560  fvsng  5570  2nd1st  6032  dfmpo  6074  cnvf1olem  6075  tpostpos  6115  tfrlemi1  6183  tfr1onlemaccex  6199  tfrcllemaccex  6212  elixpsn  6583  ixpsnf1o  6584  en1bg  6648  mapsnen  6659  xpassen  6677  fztp  9751  fzsuc2  9752  fseq1p1m1  9767  fseq1m1p1  9768  zfz1isolemsplit  10474  zfz1isolem1  10476  fsumm1  11077  divalgmod  11472  ennnfonelemg  11761  ennnfonelemp1  11764  ennnfonelem1  11765  ennnfonelemnn0  11780  setsvalg  11832  strsetsid  11835  txdis  12288