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

Theorem snnz 4145
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 4144 . 2  |-  ( A  e.  _V  ->  { A }  =/=  (/) )
31, 2ax-mp 5 1  |-  { A }  =/=  (/)
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767    =/= wne 2662   _Vcvv 3113   (/)c0 3785   {csn 4027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3115  df-dif 3479  df-nul 3786  df-sn 4028
This theorem is referenced by:  snsssn  4195  0nep0  4618  notzfaus  4622  nnullss  4709  opthwiener  4749  fparlem3  6882  fparlem4  6883  1n0  7142  fodomr  7665  mapdom3  7686  ssfii  7875  marypha1lem  7889  fseqdom  8403  dfac5lem3  8502  isfin1-3  8762  axcc2lem  8812  axdc4lem  8831  fpwwe2lem13  9016  isumltss  13619  0subg  16021  pmtrprfvalrn  16309  gsumxp  16795  gsumxpOLD  16797  lsssn0  17377  t1conperf  19703  isufil2  20144  cnextf  20301  ustuqtop1  20479  dveq0  22136  wwlknext  24400  esumnul  27699  bdayfo  29012  nobndlem3  29031  filnetlem4  29802  diophrw  30296  dfac11  30612  bnj970  33084  bj-0nelsngl  33610  bj-2upln1upl  33663  dibn0  35950
  Copyright terms: Public domain W3C validator