Theorem sneqi 4536

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

Syntax hints:   = wceq 1538  {csn 4525

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-sn 4526

This theorem is referenced by:  fnressn  6897  fressnfv  6899  snriota  7126  xpassen  8594  ids1  13942  s3tpop  14262  bpoly3  15404  strle1  16584  2strop1  16599  ghmeqker  18377  pws1  19362  pwsmgp  19364  lpival  20011  mat1dimelbas  21076  mat1dim0  21078  mat1dimid  21079  mat1dimscm  21080  mat1dimmul  21081  mat1f1o  21083  imasdsf1olem  22980  ehl0  24021  vtxval3sn  26836  iedgval3sn  26837  uspgr1v1eop  27039  hh0oi  29686  eulerpartlemmf  31743  bnj601  32302  dffv5  33498  zrdivrng  35391  isdrngo1  35394  fnimasnd  39415  prjspval2  39607  mapfzcons  39657  mapfzcons1  39658  mapfzcons2  39660  df3o3  40728  fourierdlem80  42828  lmod1zr  44902