Theorem sneqi 4579

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 4578	. 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	ax-mp 5	1 ⊢ {𝐴} = {𝐵}

Syntax hints:   = wceq 1542  {csn 4568

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-sn 4569

This theorem is referenced by:  fnressn  7106  fressnfv  7108  snriota  7351  xpassen  9003  ids1  14554  s3tpop  14865  bpoly3  16017  strle1  17122  2strop  17193  ghmeqker  19212  pws1  20298  pwsmgp  20300  lpival  21317  mat1dimelbas  22449  mat1dim0  22451  mat1dimid  22452  mat1dimscm  22453  mat1dimmul  22454  mat1f1o  22456  imasdsf1olem  24351  ehl0  25397  nosupcbv  27683  noinfcbv  27698  bday1  27823  bdaypw2n0bndlem  28472  vtxval3sn  29129  iedgval3sn  29130  uspgr1v1eop  29335  hh0oi  31992  eulerpartlemmf  34538  bnj601  35081  dffv5  36123  zrdivrng  38291  isdrngo1  38294  aks5lem3a  42645  aks5lem7  42656  prjspval2  43063  mapfzcons  43165  mapfzcons1  43166  mapfzcons2  43168  df3o3  43763  fourierdlem80  46635  lmod1zr  48984  ovsng2  49349  setc1oterm  49981  setc1ohomfval  49983  setc1ocofval  49984  funcsetc1o  49987  termcfuncval  50022  termcnatval  50025