Theorem sneqi 4410

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

Syntax hints:   = wceq 1656  {csn 4399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-sn 4400

This theorem is referenced by:  fnressn  6681  fressnfv  6683  snriota  6901  xpassen  8329  ids1  13664  s3tpop  14037  bpoly3  15168  strle1  16339  2strop1  16354  ghmeqker  18045  pws1  18977  pwsmgp  18979  lpival  19613  mat1dimelbas  20652  mat1dim0  20654  mat1dimid  20655  mat1dimscm  20656  mat1dimmul  20657  mat1f1o  20659  imasdsf1olem  22555  ehl0  23592  vtxval3sn  26348  iedgval3sn  26349  uspgr1v1eop  26553  hh0oi  29313  eulerpartlemmf  30978  bnj601  31532  dffv5  32565  zrdivrng  34293  isdrngo1  34296  mapfzcons  38122  mapfzcons1  38123  mapfzcons2  38125  df3o3  39162  fourierdlem80  41195  lmod1zr  43147