Theorem snnz 4743

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

Syntax hints:   ∈ wcel 2109   ≠ wne 2926  Vcvv 3450  ∅c0 4299  {csn 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-dif 3920  df-nul 4300  df-sn 4593

This theorem is referenced by:  snsssn  4808  0nep0  5316  notzfaus  5321  nnullss  5425  snopeqop  5469  opthwiener  5477  fparlem3  8096  fparlem4  8097  1n0  8455  fodomr  9098  mapdom3  9119  fodomfir  9286  ssfii  9377  marypha1lem  9391  djuexb  9869  fseqdom  9986  dfac5lem3  10085  isfin1-3  10346  axcc2lem  10396  axdc4lem  10415  fpwwe2lem12  10602  hash1n0  14393  s1nz  14579  isumltss  15821  0subgOLD  19091  pmtrprfvalrn  19425  gsumxp  19913  lsssn0  20861  pzriprnglem4  21401  frlmip  21694  t1connperf  23330  dissnlocfin  23423  isufil2  23802  cnextf  23960  ustuqtop1  24136  rrxip  25297  dveq0  25912  noxp1o  27582  bdayfo  27596  noetasuplem2  27653  noetasuplem4  27655  noetainflem2  27657  noetainflem4  27659  scutun12  27729  cuteq0  27751  cuteq1  27753  cofcut1  27835  addscut2  27893  sleadd1  27903  addsuniflem  27915  addsasslem1  27917  addsasslem2  27918  negscut2  27953  mulscut2  28043  wwlksnext  29830  clwwlknon1sn  30036  esumnul  34045  bnj970  34944  filnetlem4  36376  bj-0nelsngl  36966  bj-2upln1upl  37019  dibn0  41154  diophrw  42754  dfac11  43058  fucofvalne  49318