Theorem snnzg 4799

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2946  ∅c0 4352  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-dif 3979  df-nul 4353  df-sn 4649

This theorem is referenced by:  snn0d  4800  snnz  4801  frirr  5676  frsn  5787  omsucne  7922  1stconst  8141  2ndconst  8142  fczsupp0  8234  hashge3el3dif  14536  pwsbas  17547  pwsle  17552  trnei  23921  uffix  23950  neiflim  24003  flimclslem  24013  fclsfnflim  24056  ustneism  24253  ustuqtop5  24275  dv11cn  26060  noextendseq  27730  scutbdaylt  27881  lltropt  27929  snsssng  32543  cosnop  32707  elpadd2at  39763  onnog  43391  onnobdayg  43392  bdaybndbday  43394