Theorem sneqi 4600

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

Syntax hints:   = wceq 1540  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-sn 4590

This theorem is referenced by:  fnressn  7130  fressnfv  7132  snriota  7377  xpassen  9035  ids1  14562  s3tpop  14875  bpoly3  16024  strle1  17128  2strop  17199  ghmeqker  19175  pws1  20234  pwsmgp  20236  lpival  21234  mat1dimelbas  22358  mat1dim0  22360  mat1dimid  22361  mat1dimscm  22362  mat1dimmul  22363  mat1f1o  22365  imasdsf1olem  24261  ehl0  25317  nosupcbv  27614  noinfcbv  27629  bday1s  27743  vtxval3sn  28970  iedgval3sn  28971  uspgr1v1eop  29176  hh0oi  31832  eulerpartlemmf  34366  bnj601  34910  dffv5  35912  zrdivrng  37947  isdrngo1  37950  aks5lem3a  42177  aks5lem7  42188  prjspval2  42601  mapfzcons  42704  mapfzcons1  42705  mapfzcons2  42707  df3o3  43303  fourierdlem80  46184  lmod1zr  48482  ovsng2  48847  setc1oterm  49480  setc1ohomfval  49482  setc1ocofval  49483  funcsetc1o  49486  termcfuncval  49521  termcnatval  49524