Theorem sneqi 4040

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 4039	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  =wceq 1395  {csn 4029

This theorem is referenced by:  fnressn  6083  fressnfv  6085  snriota  6287  xpassen  7631  ids1  12609  strlemor1  14724  strle1  14728  ghmeqker  16293  pws1  17265  pwsmgp  17267  lpival  17893  mat1dimelbas  18973  mat1dim0  18975  mat1dimid  18976  mat1dimscm  18977  mat1dimmul  18978  mat1f1o  18980  imasdsf1olem  20876  vdgr1c  24905  ginvsn  25351  zrdivrng  25434  hh0oi  26822  eulerpartlemmf  28314  dffv5  29574  bpoly3  29820  isdrngo1  30359  mapfzcons  30648  mapfzcons1  30649  mapfzcons2  30651  fourierdlem80  31969  lmod1zr  33094  bnj601  33978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-sn 4030