Theorem sneqd 3606

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

Syntax hints:   → wi 4   = wceq 1353  {csn 3593

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-sn 3599

This theorem is referenced by:  dmsnsnsng  5107  cnvsng  5115  ressn  5170  f1osng  5503  fsng  5690  fnressn  5703  fvsng  5713  2nd1st  6181  dfmpo  6224  cnvf1olem  6225  tpostpos  6265  tfrlemi1  6333  tfr1onlemaccex  6349  tfrcllemaccex  6362  elixpsn  6735  ixpsnf1o  6736  en1bg  6800  mapsnen  6811  xpassen  6830  fztp  10078  fzsuc2  10079  fseq1p1m1  10094  fseq1m1p1  10095  zfz1isolemsplit  10818  zfz1isolem1  10820  fsumm1  11424  fprodm1  11606  divalgmod  11932  ennnfonelemg  12404  ennnfonelemp1  12407  ennnfonelem1  12408  ennnfonelemnn0  12423  setsvalg  12492  strsetsid  12495  imasex  12726  imasival  12727  imasaddvallemg  12736  mulgval  12986  isunitd  13275  txdis  13780