Theorem snnz 4730

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

Syntax hints:   ∈ wcel 2109   ≠ wne 2925  Vcvv 3438  ∅c0 4286  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-dif 3908  df-nul 4287  df-sn 4580

This theorem is referenced by:  snsssn  4795  0nep0  5300  notzfaus  5305  nnullss  5409  snopeqop  5453  opthwiener  5461  fparlem3  8054  fparlem4  8055  1n0  8413  fodomr  9052  mapdom3  9073  fodomfir  9237  ssfii  9328  marypha1lem  9342  djuexb  9824  fseqdom  9939  dfac5lem3  10038  isfin1-3  10299  axcc2lem  10349  axdc4lem  10368  fpwwe2lem12  10555  hash1n0  14346  s1nz  14532  isumltss  15773  0subgOLD  19049  pmtrprfvalrn  19385  gsumxp  19873  lsssn0  20869  pzriprnglem4  21409  frlmip  21703  t1connperf  23339  dissnlocfin  23432  isufil2  23811  cnextf  23969  ustuqtop1  24145  rrxip  25306  dveq0  25921  noxp1o  27591  bdayfo  27605  noetasuplem2  27662  noetasuplem4  27664  noetainflem2  27666  noetainflem4  27668  scutun12  27739  cuteq0  27764  cuteq1  27766  cofcut1  27851  addscut2  27909  sleadd1  27919  addsuniflem  27931  addsasslem1  27933  addsasslem2  27934  negscut2  27969  mulscut2  28059  wwlksnext  29856  clwwlknon1sn  30062  esumnul  34014  bnj970  34913  filnetlem4  36354  bj-0nelsngl  36944  bj-2upln1upl  36997  dibn0  41132  diophrw  42732  dfac11  43035  fucofvalne  49311