Theorem sneqi 4640

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

Syntax hints:   = wceq 1542  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-sn 4630

This theorem is referenced by:  fnressn  7156  fressnfv  7158  snriota  7399  xpassen  9066  ids1  14547  s3tpop  14860  bpoly3  16002  strle1  17091  2strop1  17172  ghmeqker  19119  pws1  20138  pwsmgp  20140  lpival  20883  mat1dimelbas  21973  mat1dim0  21975  mat1dimid  21976  mat1dimscm  21977  mat1dimmul  21978  mat1f1o  21980  imasdsf1olem  23879  ehl0  24934  nosupcbv  27205  noinfcbv  27220  bday1s  27332  vtxval3sn  28303  iedgval3sn  28304  uspgr1v1eop  28506  hh0oi  31156  eulerpartlemmf  33374  bnj601  33931  dffv5  34896  zrdivrng  36821  isdrngo1  36824  prjspval2  41355  mapfzcons  41454  mapfzcons1  41455  mapfzcons2  41457  df3o3  42064  fourierdlem80  44902  lmod1zr  47174  mndtchom  47710