Theorem sneqi 4595

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

This proof depends on syntax axioms:   = wceq 1570  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-sn 4589

This theorem is used by:  fnressn  7194  fressnfv  7196  snriota  7441  xpassen  9128  ids1  14785  s3tpop  15103  bpoly3  16268  strle1  17380  2strop  17451  ghmeqker  19507  pws1  20605  pwsmgp  20607  lpival  21699  mat1dimelbas  22841  mat1dim0  22843  mat1dimid  22844  mat1dimscm  22845  mat1dimmul  22846  mat1f1o  22848  imasdsf1olem  24747  ehl0  25793  nosupcbv  28116  noinfcbv  28131  bday1  28257  bdaypw2n0bndlem  28906  vtxval3sn  29678  iedgval3sn  29679  uspgr1v1eop  29887  hh0oi  32562  selvply1rhm0  34269  eulerpartlemmf  35118  bnj601  35661  dffv5  36901  zrdivrng  39153  isdrngo1  39156  aks5lem3a  43505  aks5lem7  43516  prjspval2  43907  mapfzcons  43993  mapfzcons1  43994  mapfzcons2  43996  df3o3  44577  k0004val0  45415  fourierdlem80  47469  isprmrng  49764  lmod1zr  49936  ovsng2  50301  setc1oterm  50957  setc1ohomfval  50959  setc1ocofval  50960  funcsetc1o  50963  termcfuncval  50998  termcnatval  51004