Theorem sneqi 4639

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

Hypothesis

Ref	Expression
sneqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
sneqi	⊢ {𝐴} = {𝐵}

Proof of Theorem sneqi

Step	Hyp	Ref	Expression
1		sneqi.1	. 2 ⊢ 𝐴 = 𝐵
2		sneq 4638	. 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	ax-mp 5	1 ⊢ {𝐴} = {𝐵}

Syntax hints:   = wceq 1541  {csn 4628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-sn 4629

This theorem is referenced by:  fnressn  7155  fressnfv  7157  snriota  7398  xpassen  9065  ids1  14546  s3tpop  14859  bpoly3  16001  strle1  17090  2strop1  17171  ghmeqker  19118  pws1  20137  pwsmgp  20139  lpival  20882  mat1dimelbas  21972  mat1dim0  21974  mat1dimid  21975  mat1dimscm  21976  mat1dimmul  21977  mat1f1o  21979  imasdsf1olem  23878  ehl0  24933  nosupcbv  27202  noinfcbv  27217  bday1s  27329  vtxval3sn  28300  iedgval3sn  28301  uspgr1v1eop  28503  hh0oi  31151  eulerpartlemmf  33369  bnj601  33926  dffv5  34891  zrdivrng  36816  isdrngo1  36819  prjspval2  41356  mapfzcons  41444  mapfzcons1  41445  mapfzcons2  41447  df3o3  42054  fourierdlem80  44892  lmod1zr  47164  mndtchom  47700