Theorem snn0d 4746

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

Step	Hyp	Ref	Expression
1		snn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		snnzg 4745	. 2 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅)
3	1, 2	syl 18	1 ⊢ (𝜑 → {𝐴} ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 2149   ≠ wne 2964  ∅c0 4294  {csn 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-dif 3916  df-nul 4295  df-sn 4595

This theorem is referenced by:  0nelop  5480  rnglidl0  21332  hausflim  24106  flimcf  24107  flimclslem  24109  cnpflf2  24125  cnpflf  24126  neipcfilu  24420  sltsbday  28075  zarclssn  34207  zar0ring  34212  elpaddat  40467  mnuprdlem1  44873  difmapsn  45819  ovnovollem1  47261  ovnovollem3  47263