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

Theorem snnz 4093
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 4092 . 2  |-  ( A  e.  _V  ->  { A }  =/=  (/) )
31, 2ax-mp 5 1  |-  { A }  =/=  (/)
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758    =/= wne 2644   _Vcvv 3070   (/)c0 3737   {csn 3977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-v 3072  df-dif 3431  df-nul 3738  df-sn 3978
This theorem is referenced by:  snsssn  4141  0nep0  4563  notzfaus  4567  nnullss  4654  opthwiener  4693  fparlem3  6776  fparlem4  6777  1n0  7037  fodomr  7564  mapdom3  7585  ssfii  7772  marypha1lem  7786  fseqdom  8299  dfac5lem3  8398  isfin1-3  8658  axcc2lem  8708  axdc4lem  8727  fpwwe2lem13  8912  isumltss  13415  0subg  15810  pmtrprfvalrn  16098  gsumxp  16575  gsumxpOLD  16577  lsssn0  17137  t1conperf  19158  isufil2  19599  cnextf  19756  ustuqtop1  19934  dveq0  21590  esumnul  26638  bdayfo  27952  nobndlem3  27971  filnetlem4  28742  diophrw  29237  dfac11  29555  wwlknext  30496  bnj970  32242  bj-0nelsngl  32766  bj-2upln1upl  32819  dibn0  35106
  Copyright terms: Public domain W3C validator