Theorem sneqi 4602

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

Syntax hints:   = wceq 1540  {csn 4591

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-sn 4592

This theorem is referenced by:  fnressn  7132  fressnfv  7134  snriota  7379  xpassen  9039  ids1  14568  s3tpop  14881  bpoly3  16030  strle1  17134  2strop  17205  ghmeqker  19181  pws1  20240  pwsmgp  20242  lpival  21240  mat1dimelbas  22364  mat1dim0  22366  mat1dimid  22367  mat1dimscm  22368  mat1dimmul  22369  mat1f1o  22371  imasdsf1olem  24267  ehl0  25323  nosupcbv  27620  noinfcbv  27635  bday1s  27749  vtxval3sn  28976  iedgval3sn  28977  uspgr1v1eop  29182  hh0oi  31838  eulerpartlemmf  34372  bnj601  34916  dffv5  35907  zrdivrng  37942  isdrngo1  37945  aks5lem3a  42172  aks5lem7  42183  prjspval2  42594  mapfzcons  42697  mapfzcons1  42698  mapfzcons2  42700  df3o3  43296  fourierdlem80  46177  lmod1zr  48472  ovsng2  48837  setc1oterm  49470  setc1ohomfval  49472  setc1ocofval  49473  funcsetc1o  49476  termcfuncval  49511  termcnatval  49514