Theorem sneqd 3631

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

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

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 3624

This theorem is referenced by:  dmsnsnsng  5143  cnvsng  5151  ressn  5206  f1osng  5541  fsng  5731  fnressn  5744  fvsng  5754  2nd1st  6233  dfmpo  6276  cnvf1olem  6277  tpostpos  6317  tfrlemi1  6385  tfr1onlemaccex  6401  tfrcllemaccex  6414  elixpsn  6789  ixpsnf1o  6790  en1bg  6854  mapsnen  6865  xpassen  6884  fztp  10144  fzsuc2  10145  fseq1p1m1  10160  fseq1m1p1  10161  zfz1isolemsplit  10909  zfz1isolem1  10911  fsumm1  11559  fprodm1  11741  divalgmod  12068  ennnfonelemg  12560  ennnfonelemp1  12563  ennnfonelem1  12564  ennnfonelemnn0  12579  setsvalg  12648  strsetsid  12651  imasex  12888  imasival  12889  imasaddvallemg  12898  mulgval  13192  isunitd  13602  lspsnneg  13916  lspsnsub  13917  lmodindp1  13924  lidl0  13985  rsp0  13989  ridl0  14006  zrhrhmb  14110  znval  14124  psrval  14152  txdis  14445