Theorem snnz 4730

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

Syntax hints:   ∈ wcel 2113   ≠ wne 2930  Vcvv 3438  ∅c0 4284  {csn 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2931  df-dif 3902  df-nul 4285  df-sn 4578

This theorem is referenced by:  snsssn  4794  0nep0  5300  notzfaus  5305  nnullss  5407  snopeqop  5451  opthwiener  5459  fparlem3  8053  fparlem4  8054  1n0  8412  fodomr  9051  mapdom3  9072  fodomfir  9222  ssfii  9313  marypha1lem  9327  djuexb  9812  fseqdom  9927  dfac5lem3  10026  isfin1-3  10287  axcc2lem  10337  axdc4lem  10356  fpwwe2lem12  10543  hash1n0  14338  s1nz  14525  isumltss  15765  pmtrprfvalrn  19410  gsumxp  19898  lsssn0  20891  pzriprnglem4  21431  frlmip  21725  t1connperf  23361  dissnlocfin  23454  isufil2  23833  cnextf  23991  ustuqtop1  24166  rrxip  25327  dveq0  25942  noxp1o  27612  bdayfo  27626  noetasuplem2  27683  noetasuplem4  27685  noetainflem2  27687  noetainflem4  27689  scutun12  27761  cuteq0  27786  cuteq1  27788  cofcut1  27874  addscut2  27932  sleadd1  27942  addsuniflem  27954  addsasslem1  27956  addsasslem2  27957  negscut2  27992  mulscut2  28082  wwlksnext  29882  clwwlknon1sn  30091  esumnul  34072  bnj970  34970  filnetlem4  36436  bj-0nelsngl  37026  bj-2upln1upl  37079  dibn0  41262  diophrw  42866  dfac11  43169  fucofvalne  49440