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

Theorem snnz 4703
Description: The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
Hypothesis
Ref Expression
snnz.1 𝐴 ∈ V
Assertion
Ref Expression
snnz {𝐴} ≠ ∅

Proof of Theorem snnz
StepHypRef Expression
1 snnz.1 . 2 𝐴 ∈ V
2 snnzg 4702 . 2 (𝐴 ∈ V → {𝐴} ≠ ∅)
31, 2ax-mp 5 1 {𝐴} ≠ ∅
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  wne 3014  Vcvv 3493  c0 4289  {csn 4559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-dif 3937  df-nul 4290  df-sn 4560
This theorem is referenced by:  snsssn  4764  0nep0  5249  notzfaus  5253  notzfausOLD  5254  nnullss  5345  snopeqop  5387  opthwiener  5395  fparlem3  7801  fparlem4  7802  1n0  8111  fodomr  8660  mapdom3  8681  ssfii  8875  marypha1lem  8889  djuexb  9330  fseqdom  9444  dfac5lem3  9543  isfin1-3  9800  axcc2lem  9850  axdc4lem  9869  fpwwe2lem13  10056  hash1n0  13774  s1nz  13953  isumltss  15195  0subg  18296  pmtrprfvalrn  18608  gsumxp  19088  lsssn0  19711  frlmip  20914  t1connperf  22036  dissnlocfin  22129  isufil2  22508  cnextf  22666  ustuqtop1  22842  rrxip  23985  dveq0  24589  wwlksnext  27663  clwwlknon1sn  27871  esumnul  31295  bnj970  32207  noxp1o  33158  bdayfo  33170  noetalem3  33207  noetalem4  33208  scutun12  33259  filnetlem4  33717  bj-0nelsngl  34271  bj-2upln1upl  34324  dibn0  38276  diophrw  39341  dfac11  39647
  Copyright terms: Public domain W3C validator