Theorem snnz 4712

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

Syntax hints:   ∈ wcel 2106   ≠ wne 2943  Vcvv 3429  ∅c0 4256  {csn 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-dif 3889  df-nul 4257  df-sn 4562

This theorem is referenced by:  snsssn  4772  0nep0  5278  notzfaus  5283  nnullss  5375  snopeqop  5418  opthwiener  5426  fparlem3  7941  fparlem4  7942  1n0  8305  fodomr  8902  mapdom3  8923  ssfii  9165  marypha1lem  9179  djuexb  9677  fseqdom  9792  dfac5lem3  9891  isfin1-3  10152  axcc2lem  10202  axdc4lem  10221  fpwwe2lem12  10408  hash1n0  14146  s1nz  14322  isumltss  15570  0subg  18790  pmtrprfvalrn  19106  gsumxp  19587  lsssn0  20219  frlmip  20995  t1connperf  22597  dissnlocfin  22690  isufil2  23069  cnextf  23227  ustuqtop1  23403  rrxip  24564  dveq0  25174  wwlksnext  28266  clwwlknon1sn  28472  esumnul  32024  bnj970  32935  noxp1o  33874  bdayfo  33888  noetasuplem2  33945  noetasuplem4  33947  noetainflem2  33949  noetainflem4  33951  scutun12  34012  cofcut1  34098  filnetlem4  34578  bj-0nelsngl  35169  bj-2upln1upl  35222  dibn0  39175  diophrw  40589  dfac11  40895