Theorem snnz 4740

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

This proof depends on syntax axioms:   ∈ wcel 2145   ≠ wne 2957  Vcvv 3453  ∅c0 4282  {csn 4587

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-dif 3905  df-nul 4283  df-sn 4588

This theorem is used by:  snsssn  4804  0nep0  5326  notsep  5332  nnullss  5441  snopeqop  5487  opthwiener  5495  fparlem3  8115  fparlem4  8116  1n0OLD  8479  fodomr  9130  mapdom3  9151  fodomfir  9301  ssfii  9393  marypha1lem  9407  djuexb  9918  fseqdom  10033  dfac5lem3  10132  isfin1-3  10392  axcc2lem  10442  axdc4lem  10461  fpwwe2lem12  10655  hash1n0  14490  s1nz  14678  isumltss  15941  degenmgmnfn  19055  pmtrprfvalrn  19621  gsumxp  20109  lsssn0  21138  pzriprnglem4  21703  frlmip  21997  t1connperf  23667  dissnlocfin  23761  isufil2  24140  cnextf  24298  ustuqtop1  24473  rrxip  25624  dveq0  26234  noxp1o  27907  bdayfo  27921  noetasuplem2  27978  noetasuplem4  27980  noetainflem2  27982  noetainflem4  27984  cutsun12  28063  cuteq0  28088  cuteq1  28090  cofcut1  28193  addcuts2  28252  leadds1  28262  addsuniflem  28274  addsasslem1  28276  addsasslem2  28277  negcut2  28313  mulcut2  28406  wwlksnext  30369  clwwlknon1sn  30578  esumnul  34566  bnj970  35464  filnetlem4  37008  bj-0nelsngl  37723  bj-2upln1upl  37776  dibn0  42034  diophrw  43612  dfac11  43911  fucofvalne  50259