Theorem sneqi 4578

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

Syntax hints:   = wceq 1542  {csn 4567

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-sn 4568

This theorem is referenced by:  fnressn  7112  fressnfv  7114  snriota  7357  xpassen  9009  ids1  14560  s3tpop  14871  bpoly3  16023  strle1  17128  2strop  17199  ghmeqker  19218  pws1  20304  pwsmgp  20306  lpival  21322  mat1dimelbas  22436  mat1dim0  22438  mat1dimid  22439  mat1dimscm  22440  mat1dimmul  22441  mat1f1o  22443  imasdsf1olem  24338  ehl0  25384  nosupcbv  27666  noinfcbv  27681  bday1  27806  bdaypw2n0bndlem  28455  vtxval3sn  29112  iedgval3sn  29113  uspgr1v1eop  29318  hh0oi  31974  eulerpartlemmf  34519  bnj601  35062  dffv5  36104  zrdivrng  38274  isdrngo1  38277  aks5lem3a  42628  aks5lem7  42639  prjspval2  43046  mapfzcons  43148  mapfzcons1  43149  mapfzcons2  43151  df3o3  43742  fourierdlem80  46614  lmod1zr  48969  ovsng2  49334  setc1oterm  49966  setc1ohomfval  49968  setc1ocofval  49969  funcsetc1o  49972  termcfuncval  50007  termcnatval  50010