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 2147   ≠ wne 2959  Vcvv 3454  ∅c0 4281  {csn 4588

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-dif 4050  df-nul 4282  df-sn 4589

This theorem is used by:  snsssn  4799  0nep0  5324  notsep  5330  nnullss  5435  snopeqop  5483  opthwiener  5492  fparlem3  8155  fparlem4  8156  1n0OLD  8527  fodomr  9178  mapdom3  9199  fodomfir  9350  ssfii  9441  marypha1lem  9455  djuexb  10020  fseqdom  10135  dfac5lem3  10234  isfin1-3  10494  axcc2lem  10544  axdc4lem  10563  fpwwe2lem12  10757  hash1n0  14596  s1nz  14784  isumltss  16049  degenmgmnfn  19168  pmtrprfvalrn  19735  gsumxp  20223  lsssn0  21256  pzriprnglem4  21823  frlmip  22117  t1connperf  23787  dissnlocfin  23881  isufil2  24260  cnextf  24418  ustuqtop1  24593  rrxip  25744  dveq0  26353  noxp1o  28053  bdayfo  28067  noetasuplem2  28124  noetasuplem4  28126  noetainflem2  28128  noetainflem4  28130  cutsun12  28209  cuteq0  28234  cuteq1  28236  cofcut1  28339  addcuts2  28398  leadds1  28408  addsuniflem  28420  addsasslem1  28422  addsasslem2  28423  negcut2  28459  mulcut2  28552  wwlksnext  30515  clwwlknon1sn  30724  esumnul  34763  bnj970  35660  filnetlem4  37360  bj-0nelsngl  38075  bj-2upln1upl  38128  dibn0  42413  diophrw  43974  dfac11  44268  fucofvalne  50662