Theorem sneqi 4188

Description: Equality inference for singletons. (Contributed by NM, 22-Jan-2004.)

Hypothesis

Ref	Expression
sneqi.1	|- A = B

Assertion

Ref	Expression
sneqi	|- { A } = { B }

Proof of Theorem sneqi

Step	Hyp	Ref	Expression
1		sneqi.1	. 2 |- A = B
2		sneq 4187	. 2 |- ( A = B -> { A } = { B } )
3	1, 2	ax-mp 5	1 |- { A } = { B }

Syntax hints:   = wceq 1483   {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-sn 4178

This theorem is referenced by:  fnressn  6425  fressnfv  6427  snriota  6641  xpassen  8054  ids1  13377  s3tpop  13654  bpoly3  14789  strlemor1OLD  15969  strle1  15973  2strop1  15988  ghmeqker  17687  pws1  18616  pwsmgp  18618  lpival  19245  mat1dimelbas  20277  mat1dim0  20279  mat1dimid  20280  mat1dimscm  20281  mat1dimmul  20282  mat1f1o  20284  imasdsf1olem  22178  vtxval3sn  25935  iedgval3sn  25936  uspgr1v1eop  26141  hh0oi  28762  eulerpartlemmf  30437  bnj601  30990  dffv5  32031  zrdivrng  33752  isdrngo1  33755  mapfzcons  37279  mapfzcons1  37280  mapfzcons2  37282  df3o3  38323  fourierdlem80  40403  lmod1zr  42282