Theorem snnz 4782

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

Syntax hints:   ∈ wcel 2098   ≠ wne 2929  Vcvv 3461  ∅c0 4322  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-dif 3947  df-nul 4323  df-sn 4631

This theorem is referenced by:  snsssn  4844  0nep0  5358  notzfaus  5363  nnullss  5464  snopeqop  5508  opthwiener  5516  fparlem3  8119  fparlem4  8120  1n0  8509  fodomr  9153  mapdom3  9174  ssfii  9444  marypha1lem  9458  djuexb  9934  fseqdom  10051  dfac5lem3  10150  isfin1-3  10411  axcc2lem  10461  axdc4lem  10480  fpwwe2lem12  10667  hash1n0  14416  s1nz  14593  isumltss  15830  0subgOLD  19115  pmtrprfvalrn  19455  gsumxp  19943  lsssn0  20844  pzriprnglem4  21427  frlmip  21729  t1connperf  23384  dissnlocfin  23477  isufil2  23856  cnextf  24014  ustuqtop1  24190  rrxip  25362  dveq0  25977  noxp1o  27642  bdayfo  27656  noetasuplem2  27713  noetasuplem4  27715  noetainflem2  27717  noetainflem4  27719  scutun12  27789  cuteq0  27811  cuteq1  27812  cofcut1  27886  addscut2  27942  sleadd1  27952  addsuniflem  27964  addsasslem1  27966  addsasslem2  27967  negscut2  27998  mulscut2  28083  wwlksnext  29776  clwwlknon1sn  29982  esumnul  33798  bnj970  34709  filnetlem4  35996  bj-0nelsngl  36581  bj-2upln1upl  36634  dibn0  40756  diophrw  42321  dfac11  42628