Theorem snn0d 4739

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2957  ∅c0 4282  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-dif 3905  df-nul 4283  df-sn 4588

This theorem is used by:  0nelop  5477  rnglidl0  21424  hausflim  24213  flimcf  24214  flimclslem  24216  cnpflf2  24232  cnpflf  24233  neipcfilu  24527  sltsbday  28190  zarclssn  34391  zar0ring  34396  elpaddat  40685  mnuprdlem1  45104  difmapsn  46050  ovnovollem1  47492  ovnovollem3  47494