Theorem snnz 4781

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

Syntax hints:   ∈ wcel 2107   ≠ wne 2941  Vcvv 3475  ∅c0 4323  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-dif 3952  df-nul 4324  df-sn 4630

This theorem is referenced by:  snsssn  4843  0nep0  5357  notzfaus  5362  nnullss  5463  snopeqop  5507  opthwiener  5515  fparlem3  8100  fparlem4  8101  1n0  8488  fodomr  9128  mapdom3  9149  ssfii  9414  marypha1lem  9428  djuexb  9904  fseqdom  10021  dfac5lem3  10120  isfin1-3  10381  axcc2lem  10431  axdc4lem  10450  fpwwe2lem12  10637  hash1n0  14381  s1nz  14557  isumltss  15794  0subgOLD  19032  pmtrprfvalrn  19356  gsumxp  19844  lsssn0  20558  frlmip  21333  t1connperf  22940  dissnlocfin  23033  isufil2  23412  cnextf  23570  ustuqtop1  23746  rrxip  24907  dveq0  25517  noxp1o  27166  bdayfo  27180  noetasuplem2  27237  noetasuplem4  27239  noetainflem2  27241  noetainflem4  27243  scutun12  27311  cuteq0  27333  cuteq1  27334  cofcut1  27407  addscut2  27463  sleadd1  27472  addsuniflem  27484  addsasslem1  27486  addsasslem2  27487  negscut2  27514  mulscut2  27589  wwlksnext  29147  clwwlknon1sn  29353  esumnul  33046  bnj970  33958  filnetlem4  35266  bj-0nelsngl  35852  bj-2upln1upl  35905  dibn0  40024  diophrw  41497  dfac11  41804  pzriprnglem4  46808