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

Theorem snnz 3744
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 3743 . 2  |-  ( A  e.  _V  ->  { A }  =/=  (/) )
31, 2ax-mp 8 1  |-  { A }  =/=  (/)
Colors of variables: wff set class
Syntax hints:    e. wcel 1684    =/= wne 2446   _Vcvv 2788   (/)c0 3455   {csn 3640
This theorem is referenced by:  snsssn  3781  0nep0  4181  notzfaus  4185  nnullss  4235  opthwiener  4268  fparlem3  6220  fparlem4  6221  1n0  6494  fodomr  7012  mapdom3  7033  ssfii  7172  marypha1lem  7186  fseqdom  7653  dfac5lem3  7752  isfin1-3  8012  axcc2lem  8062  axdc4lem  8081  fpwwe2lem13  8264  isumltss  12307  0subg  14642  gsumxp  15227  lsssn0  15705  t1conperf  17162  isufil2  17603  dveq0  19347  bdayfo  23740  nobndlem3  23759  filnetlem4  25742  diophrw  26250  dfac11  26572  bnj970  28352  dibn0  30716
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-nul 3456  df-sn 3646
  Copyright terms: Public domain W3C validator