Theorem snnz 4740

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

Syntax hints:   ∈ wcel 2109   ≠ wne 2925  Vcvv 3447  ∅c0 4296  {csn 4589

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 3917  df-nul 4297  df-sn 4590

This theorem is referenced by:  snsssn  4805  0nep0  5313  notzfaus  5318  nnullss  5422  snopeqop  5466  opthwiener  5474  fparlem3  8093  fparlem4  8094  1n0  8452  fodomr  9092  mapdom3  9113  fodomfir  9279  ssfii  9370  marypha1lem  9384  djuexb  9862  fseqdom  9979  dfac5lem3  10078  isfin1-3  10339  axcc2lem  10389  axdc4lem  10408  fpwwe2lem12  10595  hash1n0  14386  s1nz  14572  isumltss  15814  0subgOLD  19084  pmtrprfvalrn  19418  gsumxp  19906  lsssn0  20854  pzriprnglem4  21394  frlmip  21687  t1connperf  23323  dissnlocfin  23416  isufil2  23795  cnextf  23953  ustuqtop1  24129  rrxip  25290  dveq0  25905  noxp1o  27575  bdayfo  27589  noetasuplem2  27646  noetasuplem4  27648  noetainflem2  27650  noetainflem4  27652  scutun12  27722  cuteq0  27744  cuteq1  27746  cofcut1  27828  addscut2  27886  sleadd1  27896  addsuniflem  27908  addsasslem1  27910  addsasslem2  27911  negscut2  27946  mulscut2  28036  wwlksnext  29823  clwwlknon1sn  30029  esumnul  34038  bnj970  34937  filnetlem4  36369  bj-0nelsngl  36959  bj-2upln1upl  37012  dibn0  41147  diophrw  42747  dfac11  43051  fucofvalne  49314