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

Theorem snnz 4081
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 4080 . 2  |-  ( A  e.  _V  ->  { A }  =/=  (/) )
31, 2ax-mp 5 1  |-  { A }  =/=  (/)
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1904    =/= wne 2641   _Vcvv 3031   (/)c0 3722   {csn 3959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-v 3033  df-dif 3393  df-nul 3723  df-sn 3960
This theorem is referenced by:  snsssn  4132  0nep0  4572  notzfaus  4576  nnullss  4662  opthwiener  4703  fparlem3  6917  fparlem4  6918  1n0  7215  fodomr  7741  mapdom3  7762  ssfii  7951  marypha1lem  7965  fseqdom  8475  dfac5lem3  8574  isfin1-3  8834  axcc2lem  8884  axdc4lem  8903  fpwwe2lem13  9085  isumltss  13983  0subg  16920  pmtrprfvalrn  17207  gsumxp  17686  lsssn0  18249  frlmip  19413  t1conperf  20528  dissnlocfin  20621  isufil2  21001  cnextf  21159  ustuqtop1  21334  rrxip  22427  dveq0  23031  wwlknext  25531  esumnul  28943  bnj970  29830  bdayfo  30635  nobndlem3  30654  filnetlem4  31108  bj-0nelsngl  31635  bj-2upln1upl  31688  dibn0  34792  diophrw  35672  dfac11  35991  hash1n0  39219  1wlkvtxiedg  39827
  Copyright terms: Public domain W3C validator