Theorem snn0d 4743

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ≠ wne 2960  ∅c0 4286  {csn 4591

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-dif 3909  df-nul 4287  df-sn 4592

This theorem is used by:  0nelop  5481  rnglidl0  21405  hausflim  24189  flimcf  24190  flimclslem  24192  cnpflf2  24208  cnpflf  24209  neipcfilu  24503  sltsbday  28161  zarclssn  34327  zar0ring  34332  elpaddat  40636  mnuprdlem1  45040  difmapsn  45986  ovnovollem1  47428  ovnovollem3  47430