Theorem snnz 4148

Description: The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)

Hypothesis

Ref	Expression
snnz.1

Assertion

Ref	Expression
snnz

Proof of Theorem snnz

Step	Hyp	Ref	Expression
1		snnz.1	. 2
2		snnzg 4147	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  e.wcel 1818  =/=wne 2652  cvv 3109  c0 3784  {csn 4029

This theorem is referenced by:  snsssn  4198  0nep0  4623  notzfaus  4627  nnullss  4714  opthwiener  4754  fparlem3  6902  fparlem4  6903  1n0  7164  fodomr  7688  mapdom3  7709  ssfii  7899  marypha1lem  7913  fseqdom  8428  dfac5lem3  8527  isfin1-3  8787  axcc2lem  8837  axdc4lem  8856  fpwwe2lem13  9041  isumltss  13660  0subg  16226  pmtrprfvalrn  16513  gsumxp  17004  gsumxpOLD  17006  lsssn0  17594  frlmip  18809  t1conperf  19937  dissnlocfin  20030  isufil2  20409  cnextf  20566  ustuqtop1  20744  rrxip  21822  dveq0  22401  wwlknext  24724  esumnul  28059  bdayfo  29435  nobndlem3  29454  filnetlem4  30199  diophrw  30692  dfac11  31008  bnj970  34005  bj-0nelsngl  34529  bj-2upln1upl  34582  dibn0  36880

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-nfc 2607  df-ne 2654  df-v 3111  df-dif 3478  df-nul 3785  df-sn 4030