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

Theorem snn0d 4780
Description: The singleton of a set is not empty. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
Hypothesis
Ref Expression
snn0d.1 (𝜑𝐴𝑉)
Assertion
Ref Expression
snn0d (𝜑 → {𝐴} ≠ ∅)

Proof of Theorem snn0d
StepHypRef Expression
1 snn0d.1 . 2 (𝜑𝐴𝑉)
2 snnzg 4779 . 2 (𝐴𝑉 → {𝐴} ≠ ∅)
31, 2syl 17 1 (𝜑 → {𝐴} ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  wne 2938  c0 4339  {csn 4631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-dif 3966  df-nul 4340  df-sn 4632
This theorem is referenced by:  0nelop  5506  rnglidl0  21257  hausflim  24005  flimcf  24006  flimclslem  24008  cnpflf2  24024  cnpflf  24025  neipcfilu  24321  zarclssn  33834  zar0ring  33839  elpaddat  39787  mnuprdlem1  44268  difmapsn  45155  ovnovollem1  46612  ovnovollem3  46614
  Copyright terms: Public domain W3C validator