Theorem snn0d 4741

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 4740	. 2 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅)
3	1, 2	syl 18	1 ⊢ (𝜑 → {𝐴} ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 2143   ≠ wne 2958  ∅c0 4286  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-dif 3908  df-nul 4287  df-sn 4590

This theorem is referenced by:  0nelop  5479  rnglidl0  21355  hausflim  24138  flimcf  24139  flimclslem  24141  cnpflf2  24157  cnpflf  24158  neipcfilu  24452  sltsbday  28110  zarclssn  34263  zar0ring  34268  elpaddat  40578  mnuprdlem1  44982  difmapsn  45928  ovnovollem1  47370  ovnovollem3  47372