Theorem snnz 4715

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

Syntax hints:   ∈ wcel 2119   ≠ wne 2935  Vcvv 3432  ∅c0 4268  {csn 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-dif 3893  df-nul 4269  df-sn 4563

This theorem is referenced by:  snsssn  4779  0nep0  5293  notzfaus  5299  nnullss  5408  snopeqop  5454  opthwiener  5462  fparlem3  8060  fparlem4  8061  1n0  8420  fodomr  9063  mapdom3  9084  fodomfir  9235  ssfii  9329  marypha1lem  9343  djuexb  9831  fseqdom  9946  dfac5lem3  10045  isfin1-3  10306  axcc2lem  10356  axdc4lem  10375  fpwwe2lem12  10563  hash1n0  14381  s1nz  14568  isumltss  15811  pmtrprfvalrn  19461  gsumxp  19949  lsssn0  20945  pzriprnglem4  21466  frlmip  21760  t1connperf  23426  dissnlocfin  23519  isufil2  23898  cnextf  24056  ustuqtop1  24231  rrxip  25382  dveq0  25992  noxp1o  27652  bdayfo  27666  noetasuplem2  27723  noetasuplem4  27725  noetainflem2  27727  noetainflem4  27729  cutsun12  27807  cuteq0  27832  cuteq1  27834  cofcut1  27937  addcuts2  27996  leadds1  28006  addsuniflem  28018  addsasslem1  28020  addsasslem2  28021  negcut2  28057  mulcut2  28150  wwlksnext  29986  clwwlknon1sn  30195  esumnul  34239  bnj970  35136  filnetlem4  36616  bj-0nelsngl  37331  bj-2upln1upl  37384  dibn0  41652  diophrw  43215  dfac11  43514  fucofvalne  49822