Theorem sneqi 4659

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

Syntax hints:   = wceq 1537  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-sn 4649

This theorem is referenced by:  fnressn  7192  fressnfv  7194  snriota  7438  xpassen  9132  ids1  14645  s3tpop  14958  bpoly3  16106  strle1  17205  2strop1  17286  ghmeqker  19283  pws1  20348  pwsmgp  20350  lpival  21357  mat1dimelbas  22498  mat1dim0  22500  mat1dimid  22501  mat1dimscm  22502  mat1dimmul  22503  mat1f1o  22505  imasdsf1olem  24404  ehl0  25470  nosupcbv  27765  noinfcbv  27780  bday1s  27894  cutpw2  28435  pw2bday  28436  vtxval3sn  29078  iedgval3sn  29079  uspgr1v1eop  29284  hh0oi  31935  eulerpartlemmf  34340  bnj601  34896  dffv5  35888  zrdivrng  37913  isdrngo1  37916  aks5lem3a  42146  aks5lem7  42157  prjspval2  42568  mapfzcons  42672  mapfzcons1  42673  mapfzcons2  42675  df3o3  43276  fourierdlem80  46107  lmod1zr  48222  mndtchom  48757