Theorem snnz 4742

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

Syntax hints:   ∈ wcel 2106   ≠ wne 2939  Vcvv 3446  ∅c0 4287  {csn 4591

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-dif 3916  df-nul 4288  df-sn 4592

This theorem is referenced by:  snsssn  4804  0nep0  5318  notzfaus  5323  nnullss  5424  snopeqop  5468  opthwiener  5476  fparlem3  8051  fparlem4  8052  1n0  8439  fodomr  9079  mapdom3  9100  ssfii  9364  marypha1lem  9378  djuexb  9854  fseqdom  9971  dfac5lem3  10070  isfin1-3  10331  axcc2lem  10381  axdc4lem  10400  fpwwe2lem12  10587  hash1n0  14331  s1nz  14507  isumltss  15744  0subgOLD  18968  pmtrprfvalrn  19284  gsumxp  19767  lsssn0  20465  frlmip  21221  t1connperf  22824  dissnlocfin  22917  isufil2  23296  cnextf  23454  ustuqtop1  23630  rrxip  24791  dveq0  25401  noxp1o  27048  bdayfo  27062  noetasuplem2  27119  noetasuplem4  27121  noetainflem2  27123  noetainflem4  27125  scutun12  27192  cuteq0  27214  cofcut1  27282  sleadd1  27341  addsunif  27353  addsasslem1  27354  addsasslem2  27355  negscut2  27381  wwlksnext  28901  clwwlknon1sn  29107  esumnul  32736  bnj970  33648  filnetlem4  34929  bj-0nelsngl  35515  bj-2upln1upl  35568  dibn0  39689  diophrw  41140  dfac11  41447