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

Theorem snnz 3867
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 3866 . 2  |-  ( A  e.  _V  ->  { A }  =/=  (/) )
31, 2ax-mp 8 1  |-  { A }  =/=  (/)
Colors of variables: wff set class
Syntax hints:    e. wcel 1717    =/= wne 2552   _Vcvv 2901   (/)c0 3573   {csn 3759
This theorem is referenced by:  snsssn  3911  0nep0  4313  notzfaus  4317  nnullss  4368  opthwiener  4401  fparlem3  6389  fparlem4  6390  1n0  6677  fodomr  7196  mapdom3  7217  ssfii  7361  marypha1lem  7375  fseqdom  7842  dfac5lem3  7941  isfin1-3  8201  axcc2lem  8251  axdc4lem  8270  fpwwe2lem13  8452  isumltss  12557  0subg  14894  gsumxp  15479  lsssn0  15953  t1conperf  17422  isufil2  17863  cnextf  18020  ustuqtop1  18194  dveq0  19753  esumnul  24241  bdayfo  25355  nobndlem3  25374  filnetlem4  26103  diophrw  26510  dfac11  26831  bnj970  28658  dibn0  31270
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-v 2903  df-dif 3268  df-nul 3574  df-sn 3765
  Copyright terms: Public domain W3C validator