MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snn0d Structured version   Visualization version   GIF version

Theorem snn0d 4774
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
StepHypRef Expression
1 snn0d.1 . 2 (𝜑𝐴𝑉)
2 snnzg 4773 . 2 (𝐴𝑉 → {𝐴} ≠ ∅)
31, 2syl 17 1 (𝜑 → {𝐴} ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wne 2939  c0 4332  {csn 4625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-dif 3953  df-nul 4333  df-sn 4626
This theorem is referenced by:  0nelop  5500  rnglidl0  21240  hausflim  23990  flimcf  23991  flimclslem  23993  cnpflf2  24009  cnpflf  24010  neipcfilu  24306  zarclssn  33873  zar0ring  33878  elpaddat  39807  mnuprdlem1  44296  difmapsn  45222  ovnovollem1  46676  ovnovollem3  46678
  Copyright terms: Public domain W3C validator