Theorem snnz 4776

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 4774	. 2 ⊢ (𝐴 ∈ V → {𝐴} ≠ ∅)
3	1, 2	ax-mp 5	1 ⊢ {𝐴} ≠ ∅

Syntax hints:   ∈ wcel 2108   ≠ wne 2940  Vcvv 3480  ∅c0 4333  {csn 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-dif 3954  df-nul 4334  df-sn 4627

This theorem is referenced by:  snsssn  4841  0nep0  5358  notzfaus  5363  nnullss  5467  snopeqop  5511  opthwiener  5519  fparlem3  8139  fparlem4  8140  1n0  8526  fodomr  9168  mapdom3  9189  fodomfir  9368  ssfii  9459  marypha1lem  9473  djuexb  9949  fseqdom  10066  dfac5lem3  10165  isfin1-3  10426  axcc2lem  10476  axdc4lem  10495  fpwwe2lem12  10682  hash1n0  14460  s1nz  14645  isumltss  15884  0subgOLD  19170  pmtrprfvalrn  19506  gsumxp  19994  lsssn0  20946  pzriprnglem4  21495  frlmip  21798  t1connperf  23444  dissnlocfin  23537  isufil2  23916  cnextf  24074  ustuqtop1  24250  rrxip  25424  dveq0  26039  noxp1o  27708  bdayfo  27722  noetasuplem2  27779  noetasuplem4  27781  noetainflem2  27783  noetainflem4  27785  scutun12  27855  cuteq0  27877  cuteq1  27878  cofcut1  27954  addscut2  28012  sleadd1  28022  addsuniflem  28034  addsasslem1  28036  addsasslem2  28037  negscut2  28072  mulscut2  28159  wwlksnext  29913  clwwlknon1sn  30119  esumnul  34049  bnj970  34961  filnetlem4  36382  bj-0nelsngl  36972  bj-2upln1upl  37025  dibn0  41155  diophrw  42770  dfac11  43074  fucofvalne  49020