Theorem snnz 4720

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

Syntax hints:   ∈ wcel 2114   ≠ wne 2932  Vcvv 3429  ∅c0 4273  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-dif 3892  df-nul 4274  df-sn 4568

This theorem is referenced by:  snsssn  4784  0nep0  5299  notzfaus  5305  nnullss  5414  snopeqop  5460  opthwiener  5468  fparlem3  8064  fparlem4  8065  1n0  8423  fodomr  9066  mapdom3  9087  fodomfir  9238  ssfii  9332  marypha1lem  9346  djuexb  9833  fseqdom  9948  dfac5lem3  10047  isfin1-3  10308  axcc2lem  10358  axdc4lem  10377  fpwwe2lem12  10565  hash1n0  14383  s1nz  14570  isumltss  15813  pmtrprfvalrn  19463  gsumxp  19951  lsssn0  20943  pzriprnglem4  21464  frlmip  21758  t1connperf  23401  dissnlocfin  23494  isufil2  23873  cnextf  24031  ustuqtop1  24206  rrxip  25357  dveq0  25967  noxp1o  27627  bdayfo  27641  noetasuplem2  27698  noetasuplem4  27700  noetainflem2  27702  noetainflem4  27704  cutsun12  27782  cuteq0  27807  cuteq1  27809  cofcut1  27912  addcuts2  27971  leadds1  27981  addsuniflem  27993  addsasslem1  27995  addsasslem2  27996  negcut2  28032  mulcut2  28125  wwlksnext  29961  clwwlknon1sn  30170  esumnul  34192  bnj970  35089  filnetlem4  36563  bj-0nelsngl  37278  bj-2upln1upl  37331  dibn0  41599  diophrw  43191  dfac11  43490  fucofvalne  49800