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

Theorem snnz 3981
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 3980 . 2  |-  ( A  e.  _V  ->  { A }  =/=  (/) )
31, 2ax-mp 5 1  |-  { A }  =/=  (/)
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755    =/= wne 2596   _Vcvv 2962   (/)c0 3625   {csn 3865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-v 2964  df-dif 3319  df-nul 3626  df-sn 3866
This theorem is referenced by:  snsssn  4029  0nep0  4451  notzfaus  4455  nnullss  4542  opthwiener  4581  fparlem3  6663  fparlem4  6664  1n0  6923  fodomr  7450  mapdom3  7471  ssfii  7657  marypha1lem  7671  fseqdom  8184  dfac5lem3  8283  isfin1-3  8543  axcc2lem  8593  axdc4lem  8612  fpwwe2lem13  8796  isumltss  13293  0subg  15685  pmtrprfvalrn  15973  gsumxp  16441  gsumxpOLD  16443  lsssn0  16950  t1conperf  18881  isufil2  19322  cnextf  19479  ustuqtop1  19657  dveq0  21313  esumnul  26355  bdayfo  27662  nobndlem3  27681  filnetlem4  28443  diophrw  28939  dfac11  29257  wwlknext  30199  bnj970  31639  bj-0nelsngl  32044  bj-2upln1upl  32097  dibn0  34368
  Copyright terms: Public domain W3C validator