Theorem snnz 4728

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

Syntax hints:   ∈ wcel 2113   ≠ wne 2929  Vcvv 3437  ∅c0 4282  {csn 4575

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 2930  df-dif 3901  df-nul 4283  df-sn 4576

This theorem is referenced by:  snsssn  4792  0nep0  5298  notzfaus  5303  nnullss  5405  snopeqop  5449  opthwiener  5457  fparlem3  8050  fparlem4  8051  1n0  8409  fodomr  9048  mapdom3  9069  fodomfir  9219  ssfii  9310  marypha1lem  9324  djuexb  9809  fseqdom  9924  dfac5lem3  10023  isfin1-3  10284  axcc2lem  10334  axdc4lem  10353  fpwwe2lem12  10540  hash1n0  14330  s1nz  14517  isumltss  15757  pmtrprfvalrn  19402  gsumxp  19890  lsssn0  20883  pzriprnglem4  21423  frlmip  21717  t1connperf  23352  dissnlocfin  23445  isufil2  23824  cnextf  23982  ustuqtop1  24157  rrxip  25318  dveq0  25933  noxp1o  27603  bdayfo  27617  noetasuplem2  27674  noetasuplem4  27676  noetainflem2  27678  noetainflem4  27680  scutun12  27752  cuteq0  27777  cuteq1  27779  cofcut1  27865  addscut2  27923  sleadd1  27933  addsuniflem  27945  addsasslem1  27947  addsasslem2  27948  negscut2  27983  mulscut2  28073  wwlksnext  29873  clwwlknon1sn  30082  esumnul  34082  bnj970  34980  filnetlem4  36446  bj-0nelsngl  37036  bj-2upln1upl  37089  dibn0  41272  diophrw  42876  dfac11  43179  fucofvalne  49450