Theorem snnz 4738

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

Syntax hints:   ∈ wcel 2145   ≠ wne 2960  Vcvv 3457  ∅c0 4288  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-dif 3910  df-nul 4289  df-sn 4586

This theorem is referenced by:  snsssn  4802  0nep0  5319  notzfaus  5325  nnullss  5434  snopeqop  5480  opthwiener  5488  fparlem3  8097  fparlem4  8098  1n0OLD  8461  fodomr  9104  mapdom3  9125  fodomfir  9275  ssfii  9367  marypha1lem  9381  djuexb  9883  fseqdom  9998  dfac5lem3  10097  isfin1-3  10358  axcc2lem  10408  axdc4lem  10427  fpwwe2lem12  10615  hash1n0  14448  s1nz  14635  isumltss  15892  pmtrprfvalrn  19549  gsumxp  20037  lsssn0  21038  pzriprnglem4  21594  frlmip  21888  t1connperf  23554  dissnlocfin  23647  isufil2  24026  cnextf  24184  ustuqtop1  24359  rrxip  25510  dveq0  26120  noxp1o  27785  bdayfo  27799  noetasuplem2  27856  noetasuplem4  27858  noetainflem2  27860  noetainflem4  27862  cutsun12  27941  cuteq0  27966  cuteq1  27968  cofcut1  28071  addcuts2  28130  leadds1  28140  addsuniflem  28152  addsasslem1  28154  addsasslem2  28155  negcut2  28191  mulcut2  28284  wwlksnext  30151  clwwlknon1sn  30360  esumnul  34355  bnj970  35252  filnetlem4  36754  bj-0nelsngl  37468  bj-2upln1upl  37521  dibn0  41789  diophrw  43352  dfac11  43651  fucofvalne  49954