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 3432  ∅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 3890  df-nul 4257  df-sn 4562

This theorem is referenced by:  snsssn  4772  0nep0  5280  notzfaus  5285  nnullss  5377  snopeqop  5420  opthwiener  5428  fparlem3  7954  fparlem4  7955  1n0  8318  fodomr  8915  mapdom3  8936  ssfii  9178  marypha1lem  9192  djuexb  9667  fseqdom  9782  dfac5lem3  9881  isfin1-3  10142  axcc2lem  10192  axdc4lem  10211  fpwwe2lem12  10398  hash1n0  14136  s1nz  14312  isumltss  15560  0subg  18780  pmtrprfvalrn  19096  gsumxp  19577  lsssn0  20209  frlmip  20985  t1connperf  22587  dissnlocfin  22680  isufil2  23059  cnextf  23217  ustuqtop1  23393  rrxip  24554  dveq0  25164  wwlksnext  28258  clwwlknon1sn  28464  esumnul  32016  bnj970  32927  noxp1o  33866  bdayfo  33880  noetasuplem2  33937  noetasuplem4  33939  noetainflem2  33941  noetainflem4  33943  scutun12  34004  cofcut1  34090  filnetlem4  34570  bj-0nelsngl  35161  bj-2upln1upl  35214  dibn0  39167  diophrw  40581  dfac11  40887