MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snnz Structured version   Unicode version

Theorem snnz 3923
Description: The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
Hypothesis
Ref Expression
snnz.1  |-  A  e. 
_V
Assertion
Ref Expression
snnz  |-  { A }  =/=  (/)

Proof of Theorem snnz
StepHypRef Expression
1 snnz.1 . 2  |-  A  e. 
_V
2 snnzg 3922 . 2  |-  ( A  e.  _V  ->  { A }  =/=  (/) )
31, 2ax-mp 8 1  |-  { A }  =/=  (/)
Colors of variables: wff set class
Syntax hints:    e. wcel 1726    =/= wne 2600   _Vcvv 2957   (/)c0 3629   {csn 3815
This theorem is referenced by:  snsssn  3968  0nep0  4371  notzfaus  4375  nnullss  4426  opthwiener  4459  fparlem3  6449  fparlem4  6450  1n0  6740  fodomr  7259  mapdom3  7280  ssfii  7425  marypha1lem  7439  fseqdom  7908  dfac5lem3  8007  isfin1-3  8267  axcc2lem  8317  axdc4lem  8336  fpwwe2lem13  8518  isumltss  12629  0subg  14966  gsumxp  15551  lsssn0  16025  t1conperf  17500  isufil2  17941  cnextf  18098  ustuqtop1  18272  dveq0  19885  esumnul  24444  bdayfo  25631  nobndlem3  25650  filnetlem4  26411  diophrw  26818  dfac11  27138  bnj970  29319  dibn0  31952
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-v 2959  df-dif 3324  df-nul 3630  df-sn 3821
  Copyright terms: Public domain W3C validator