Theorem snnz 4709

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

Syntax hints:   ∈ wcel 2108   ≠ wne 2942  Vcvv 3422  ∅c0 4253  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-dif 3886  df-nul 4254  df-sn 4559

This theorem is referenced by:  snsssn  4769  0nep0  5275  notzfaus  5280  nnullss  5371  snopeqop  5414  opthwiener  5422  fparlem3  7925  fparlem4  7926  1n0  8286  fodomr  8864  mapdom3  8885  ssfii  9108  marypha1lem  9122  djuexb  9598  fseqdom  9713  dfac5lem3  9812  isfin1-3  10073  axcc2lem  10123  axdc4lem  10142  fpwwe2lem12  10329  hash1n0  14064  s1nz  14240  isumltss  15488  0subg  18695  pmtrprfvalrn  19011  gsumxp  19492  lsssn0  20124  frlmip  20895  t1connperf  22495  dissnlocfin  22588  isufil2  22967  cnextf  23125  ustuqtop1  23301  rrxip  24459  dveq0  25069  wwlksnext  28159  clwwlknon1sn  28365  esumnul  31916  bnj970  32827  noxp1o  33793  bdayfo  33807  noetasuplem2  33864  noetasuplem4  33866  noetainflem2  33868  noetainflem4  33870  scutun12  33931  cofcut1  34017  filnetlem4  34497  bj-0nelsngl  35088  bj-2upln1upl  35141  dibn0  39094  diophrw  40497  dfac11  40803