Theorem snnz 4737

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

This proof depends on syntax axioms:   ∈ wcel 2145   ≠ wne 2956  Vcvv 3451  ∅c0 4279  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-dif 3902  df-nul 4280  df-sn 4585

This theorem is used by:  snsssn  4801  0nep0  5319  notsep  5325  nnullss  5430  snopeqop  5478  opthwiener  5487  fparlem3  8114  fparlem4  8115  1n0OLD  8480  fodomr  9131  mapdom3  9152  fodomfir  9303  ssfii  9395  marypha1lem  9409  djuexb  9971  fseqdom  10086  dfac5lem3  10185  isfin1-3  10445  axcc2lem  10495  axdc4lem  10514  fpwwe2lem12  10708  hash1n0  14546  s1nz  14734  isumltss  15997  degenmgmnfn  19116  pmtrprfvalrn  19682  gsumxp  20170  lsssn0  21203  pzriprnglem4  21770  frlmip  22064  t1connperf  23734  dissnlocfin  23828  isufil2  24207  cnextf  24365  ustuqtop1  24540  rrxip  25691  dveq0  26300  noxp1o  28002  bdayfo  28016  noetasuplem2  28073  noetasuplem4  28075  noetainflem2  28077  noetainflem4  28079  cutsun12  28158  cuteq0  28183  cuteq1  28185  cofcut1  28288  addcuts2  28347  leadds1  28357  addsuniflem  28369  addsasslem1  28371  addsasslem2  28372  negcut2  28408  mulcut2  28501  wwlksnext  30464  clwwlknon1sn  30673  esumnul  34662  bnj970  35560  filnetlem4  37139  bj-0nelsngl  37854  bj-2upln1upl  37907  dibn0  42178  diophrw  43723  dfac11  44022  fucofvalne  50377