Theorem snnz 4721

Description: The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)

Hypothesis

Ref	Expression
snnz.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
snnz	⊢ {𝐴} ≠ ∅

Proof of Theorem snnz

Step	Hyp	Ref	Expression
1		snnz.1	. 2 ⊢ 𝐴 ∈ V
2		snnzg 4719	. 2 ⊢ (𝐴 ∈ V → {𝐴} ≠ ∅)
3	1, 2	ax-mp 5	1 ⊢ {𝐴} ≠ ∅

Syntax hints:   ∈ wcel 2114   ≠ wne 2933  Vcvv 3430  ∅c0 4274  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-dif 3893  df-nul 4275  df-sn 4569

This theorem is referenced by:  snsssn  4785  0nep0  5295  notzfaus  5300  nnullss  5409  snopeqop  5454  opthwiener  5462  fparlem3  8057  fparlem4  8058  1n0  8416  fodomr  9059  mapdom3  9080  fodomfir  9231  ssfii  9325  marypha1lem  9339  djuexb  9824  fseqdom  9939  dfac5lem3  10038  isfin1-3  10299  axcc2lem  10349  axdc4lem  10368  fpwwe2lem12  10556  hash1n0  14374  s1nz  14561  isumltss  15804  pmtrprfvalrn  19454  gsumxp  19942  lsssn0  20934  pzriprnglem4  21474  frlmip  21768  t1connperf  23411  dissnlocfin  23504  isufil2  23883  cnextf  24041  ustuqtop1  24216  rrxip  25367  dveq0  25977  noxp1o  27641  bdayfo  27655  noetasuplem2  27712  noetasuplem4  27714  noetainflem2  27716  noetainflem4  27718  cutsun12  27796  cuteq0  27821  cuteq1  27823  cofcut1  27926  addcuts2  27985  leadds1  27995  addsuniflem  28007  addsasslem1  28009  addsasslem2  28010  negcut2  28046  mulcut2  28139  wwlksnext  29976  clwwlknon1sn  30185  esumnul  34208  bnj970  35105  filnetlem4  36579  bj-0nelsngl  37294  bj-2upln1upl  37347  dibn0  41613  diophrw  43205  dfac11  43508  fucofvalne  49812