Theorem snn0d 4736

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2955  ∅c0 4279  {csn 4584

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-dif 3902  df-nul 4280  df-sn 4585

This theorem is used by:  0nelop  5473  rnglidl0  21419  hausflim  24208  flimcf  24209  flimclslem  24211  cnpflf2  24227  cnpflf  24228  neipcfilu  24522  sltsbday  28183  zarclssn  34384  zar0ring  34389  elpaddat  40678  mnuprdlem1  45097  difmapsn  46043  ovnovollem1  47485  ovnovollem3  47487