Theorem snnz 4780

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

Syntax hints:   ∈ wcel 2105   ≠ wne 2937  Vcvv 3477  ∅c0 4338  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-dif 3965  df-nul 4339  df-sn 4631

This theorem is referenced by:  snsssn  4845  0nep0  5363  notzfaus  5368  nnullss  5472  snopeqop  5515  opthwiener  5523  fparlem3  8137  fparlem4  8138  1n0  8524  fodomr  9166  mapdom3  9187  fodomfir  9365  ssfii  9456  marypha1lem  9470  djuexb  9946  fseqdom  10063  dfac5lem3  10162  isfin1-3  10423  axcc2lem  10473  axdc4lem  10492  fpwwe2lem12  10679  hash1n0  14456  s1nz  14641  isumltss  15880  0subgOLD  19182  pmtrprfvalrn  19520  gsumxp  20008  lsssn0  20963  pzriprnglem4  21512  frlmip  21815  t1connperf  23459  dissnlocfin  23552  isufil2  23931  cnextf  24089  ustuqtop1  24265  rrxip  25437  dveq0  26053  noxp1o  27722  bdayfo  27736  noetasuplem2  27793  noetasuplem4  27795  noetainflem2  27797  noetainflem4  27799  scutun12  27869  cuteq0  27891  cuteq1  27892  cofcut1  27968  addscut2  28026  sleadd1  28036  addsuniflem  28048  addsasslem1  28050  addsasslem2  28051  negscut2  28086  mulscut2  28173  wwlksnext  29922  clwwlknon1sn  30128  esumnul  34028  bnj970  34939  filnetlem4  36363  bj-0nelsngl  36953  bj-2upln1upl  37006  dibn0  41135  diophrw  42746  dfac11  43050