Theorem sneqi 4566

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

Syntax hints:   = wceq 1547  {csn 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-sn 4556

This theorem is referenced by:  fnressn  7101  fressnfv  7103  snriota  7346  xpassen  8999  ids1  14551  s3tpop  14862  bpoly3  16014  strle1  17119  2strop  17190  ghmeqker  19209  pws1  20295  pwsmgp  20297  lpival  21317  mat1dimelbas  22454  mat1dim0  22456  mat1dimid  22457  mat1dimscm  22458  mat1dimmul  22459  mat1f1o  22461  imasdsf1olem  24356  ehl0  25402  nosupcbv  27684  noinfcbv  27699  bday1  27824  bdaypw2n0bndlem  28473  vtxval3sn  29130  iedgval3sn  29131  uspgr1v1eop  29336  hh0oi  31992  selvply1rhm0  33710  eulerpartlemmf  34559  bnj601  35102  dffv5  36150  zrdivrng  38320  isdrngo1  38323  aks5lem3a  42674  aks5lem7  42685  prjspval2  43063  mapfzcons  43165  mapfzcons1  43166  mapfzcons2  43168  df3o3  43759  fourierdlem80  46629  lmod1zr  48984  ovsng2  49349  setc1oterm  49981  setc1ohomfval  49983  setc1ocofval  49984  funcsetc1o  49987  termcfuncval  50022  termcnatval  50025