Theorem sneqi 4593

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

Syntax hints:   = wceq 1560  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-sn 4583

This theorem is referenced by:  fnressn  7141  fressnfv  7143  snriota  7386  xpassen  9043  ids1  14611  s3tpop  14922  bpoly3  16088  strle1  17194  2strop  17265  ghmeqker  19283  pws1  20373  pwsmgp  20375  lpival  21394  mat1dimelbas  22531  mat1dim0  22533  mat1dimid  22534  mat1dimscm  22535  mat1dimmul  22536  mat1f1o  22538  imasdsf1olem  24433  ehl0  25479  nosupcbv  27766  noinfcbv  27781  bday1  27907  bdaypw2n0bndlem  28556  vtxval3sn  29244  iedgval3sn  29245  uspgr1v1eop  29450  hh0oi  32106  selvply1rhm0  33823  eulerpartlemmf  34672  bnj601  35215  dffv5  36272  zrdivrng  38452  isdrngo1  38455  aks5lem3a  42806  aks5lem7  42817  prjspval2  43195  mapfzcons  43297  mapfzcons1  43298  mapfzcons2  43300  df3o3  43891  fourierdlem80  46760  lmod1zr  49115  ovsng2  49480  setc1oterm  50112  setc1ohomfval  50114  setc1ocofval  50115  funcsetc1o  50118  termcfuncval  50153  termcnatval  50156