Theorem snnzg 4735

Description: The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)

Assertion

Ref	Expression
snnzg	⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅)

Proof of Theorem snnzg

Step	Hyp	Ref	Expression
1		snidg 4621	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})
2	1	ne0d 4288	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:  snn0d  4736  snnz  4737  frirr  5631  frsn  5743  omsucne  7882  1stconst  8098  2ndconst  8099  fczsupp0  8192  hashge3el3dif  14555  pwsbas  17575  pwsle  17581  trnei  24121  uffix  24150  neiflim  24203  flimclslem  24213  fclsfnflim  24256  ustneism  24453  ustuqtop5  24474  dv11cn  26231  noextendseq  27906  cutbdaylt  28066  eqcuts3  28072  lltr  28130  snsssng  32992  cosnop  33170  mh-inf3sn  37164  elpadd2at  40682  onnoxpg  44272  onnobdayg  44273  bdaybndbday  44275