Theorem snnz 4747

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

This proof depends on syntax axioms:   ∈ wcel 2146   ≠ wne 2961  Vcvv 3458  ∅c0 4289  {csn 4594

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-dif 3911  df-nul 4290  df-sn 4595

This theorem is used by:  snsssn  4811  0nep0  5333  notsep  5339  nnullss  5448  snopeqop  5494  opthwiener  5502  fparlem3  8118  fparlem4  8119  1n0OLD  8482  fodomr  9126  mapdom3  9147  fodomfir  9297  ssfii  9389  marypha1lem  9403  djuexb  9914  fseqdom  10029  dfac5lem3  10128  isfin1-3  10388  axcc2lem  10438  axdc4lem  10457  fpwwe2lem12  10645  hash1n0  14478  s1nz  14666  isumltss  15928  pmtrprfvalrn  19589  gsumxp  20077  lsssn0  21106  pzriprnglem4  21671  frlmip  21965  t1connperf  23630  dissnlocfin  23723  isufil2  24102  cnextf  24260  ustuqtop1  24435  rrxip  25586  dveq0  26196  noxp1o  27864  bdayfo  27878  noetasuplem2  27935  noetasuplem4  27937  noetainflem2  27939  noetainflem4  27941  cutsun12  28020  cuteq0  28045  cuteq1  28047  cofcut1  28150  addcuts2  28209  leadds1  28219  addsuniflem  28231  addsasslem1  28233  addsasslem2  28234  negcut2  28270  mulcut2  28363  wwlksnext  30279  clwwlknon1sn  30488  esumnul  34469  bnj970  35367  filnetlem4  36933  bj-0nelsngl  37648  bj-2upln1upl  37701  dibn0  41968  diophrw  43531  dfac11  43830  fucofvalne  50144