Theorem snnz 4801

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

Syntax hints:   ∈ wcel 2108   ≠ wne 2946  Vcvv 3488  ∅c0 4352  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-dif 3979  df-nul 4353  df-sn 4649

This theorem is referenced by:  snsssn  4866  0nep0  5376  notzfaus  5381  nnullss  5482  snopeqop  5525  opthwiener  5533  fparlem3  8155  fparlem4  8156  1n0  8544  fodomr  9194  mapdom3  9215  fodomfir  9396  ssfii  9488  marypha1lem  9502  djuexb  9978  fseqdom  10095  dfac5lem3  10194  isfin1-3  10455  axcc2lem  10505  axdc4lem  10524  fpwwe2lem12  10711  hash1n0  14470  s1nz  14655  isumltss  15896  0subgOLD  19192  pmtrprfvalrn  19530  gsumxp  20018  lsssn0  20969  pzriprnglem4  21518  frlmip  21821  t1connperf  23465  dissnlocfin  23558  isufil2  23937  cnextf  24095  ustuqtop1  24271  rrxip  25443  dveq0  26059  noxp1o  27726  bdayfo  27740  noetasuplem2  27797  noetasuplem4  27799  noetainflem2  27801  noetainflem4  27803  scutun12  27873  cuteq0  27895  cuteq1  27896  cofcut1  27972  addscut2  28030  sleadd1  28040  addsuniflem  28052  addsasslem1  28054  addsasslem2  28055  negscut2  28090  mulscut2  28177  wwlksnext  29926  clwwlknon1sn  30132  esumnul  34012  bnj970  34923  filnetlem4  36347  bj-0nelsngl  36937  bj-2upln1upl  36990  dibn0  41110  diophrw  42715  dfac11  43019