Theorem snnz 4252

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

Syntax hints:   ∈ wcel 1977   ≠ wne 2780  Vcvv 3173  ∅c0 3874  {csn 4125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-v 3175  df-dif 3543  df-nul 3875  df-sn 4126

This theorem is referenced by:  snsssn  4312  0nep0  4762  notzfaus  4766  nnullss  4857  opthwiener  4901  fparlem3  7166  fparlem4  7167  1n0  7462  fodomr  7996  mapdom3  8017  ssfii  8208  marypha1lem  8222  fseqdom  8732  dfac5lem3  8831  isfin1-3  9091  axcc2lem  9141  axdc4lem  9160  fpwwe2lem13  9343  s1nz  13239  isumltss  14419  0subg  17442  pmtrprfvalrn  17731  gsumxp  18198  lsssn0  18769  frlmip  19936  t1conperf  21049  dissnlocfin  21142  isufil2  21522  cnextf  21680  ustuqtop1  21855  rrxip  22986  dveq0  23567  wwlknext  26252  esumnul  29437  bnj970  30271  bdayfo  31074  nobndlem3  31093  filnetlem4  31546  bj-0nelsngl  32152  bj-2upln1upl  32205  dibn0  35460  diophrw  36340  dfac11  36650  hash1n0  40370  wwlksnext  41099