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

Theorem snnz 4134
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 4133 . 2  |-  ( A  e.  _V  ->  { A }  =/=  (/) )
31, 2ax-mp 5 1  |-  { A }  =/=  (/)
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1823    =/= wne 2649   _Vcvv 3106   (/)c0 3783   {csn 4016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-v 3108  df-dif 3464  df-nul 3784  df-sn 4017
This theorem is referenced by:  snsssn  4184  0nep0  4608  notzfaus  4612  nnullss  4699  opthwiener  4738  fparlem3  6875  fparlem4  6876  1n0  7137  fodomr  7661  mapdom3  7682  ssfii  7871  marypha1lem  7885  fseqdom  8398  dfac5lem3  8497  isfin1-3  8757  axcc2lem  8807  axdc4lem  8826  fpwwe2lem13  9009  isumltss  13745  0subg  16428  pmtrprfvalrn  16715  gsumxp  17203  lsssn0  17792  frlmip  18983  t1conperf  20106  dissnlocfin  20199  isufil2  20578  cnextf  20735  ustuqtop1  20913  rrxip  21991  dveq0  22570  wwlknext  24929  esumnul  28280  bdayfo  29678  nobndlem3  29697  filnetlem4  30442  diophrw  30934  dfac11  31250  bnj970  34425  bj-0nelsngl  34949  bj-2upln1upl  35002  dibn0  37296
  Copyright terms: Public domain W3C validator