Theorem snnzg 4733

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 4619	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})
2	1	ne0d 4294	1 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 2142   ≠ wne 2957  ∅c0 4285  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-dif 3907  df-nul 4286  df-sn 4583

This theorem is referenced by:  snn0d  4734  snnz  4735  frirr  5623  frsn  5735  omsucne  7865  1stconst  8079  2ndconst  8080  fczsupp0  8173  hashge3el3dif  14500  pwsbas  17516  pwsle  17522  trnei  23952  uffix  23981  neiflim  24034  flimclslem  24044  fclsfnflim  24087  ustneism  24284  ustuqtop5  24305  dv11cn  26063  noextendseq  27731  cutbdaylt  27891  eqcuts3  27897  lltr  27955  snsssng  32713  cosnop  32897  mh-inf3sn  36902  elpadd2at  40430  onnoxpg  44005  onnobdayg  44006  bdaybndbday  44008