Theorem snnz 4734

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

Syntax hints:   ∈ wcel 2141   ≠ wne 2956  Vcvv 3453  ∅c0 4285  {csn 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-dif 3907  df-nul 4286  df-sn 4582

This theorem is referenced by:  snsssn  4798  0nep0  5313  notzfaus  5319  nnullss  5428  snopeqop  5474  opthwiener  5482  fparlem3  8088  fparlem4  8089  1n0OLD  8452  fodomr  9096  mapdom3  9117  fodomfir  9268  ssfii  9362  marypha1lem  9376  djuexb  9864  fseqdom  9979  dfac5lem3  10078  isfin1-3  10340  axcc2lem  10390  axdc4lem  10409  fpwwe2lem12  10597  hash1n0  14431  s1nz  14618  isumltss  15861  pmtrprfvalrn  19511  gsumxp  19999  lsssn0  20995  pzriprnglem4  21516  frlmip  21810  t1connperf  23476  dissnlocfin  23569  isufil2  23948  cnextf  24106  ustuqtop1  24281  rrxip  25432  dveq0  26042  noxp1o  27704  bdayfo  27718  noetasuplem2  27775  noetasuplem4  27777  noetainflem2  27779  noetainflem4  27781  cutsun12  27860  cuteq0  27885  cuteq1  27887  cofcut1  27990  addcuts2  28049  leadds1  28059  addsuniflem  28071  addsasslem1  28073  addsasslem2  28074  negcut2  28110  mulcut2  28203  wwlksnext  30039  clwwlknon1sn  30248  esumnul  34306  bnj970  35206  filnetlem4  36705  bj-0nelsngl  37420  bj-2upln1upl  37473  dibn0  41741  diophrw  43304  dfac11  43603  fucofvalne  49910