Theorem snnz 4704

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

Syntax hints:   ∈ wcel 2110   ≠ wne 3016  Vcvv 3494  ∅c0 4290  {csn 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-dif 3938  df-nul 4291  df-sn 4561

This theorem is referenced by:  snsssn  4765  0nep0  5250  notzfaus  5254  notzfausOLD  5255  nnullss  5346  snopeqop  5388  opthwiener  5396  fparlem3  7803  fparlem4  7804  1n0  8113  fodomr  8662  mapdom3  8683  ssfii  8877  marypha1lem  8891  djuexb  9332  fseqdom  9446  dfac5lem3  9545  isfin1-3  9802  axcc2lem  9852  axdc4lem  9871  fpwwe2lem13  10058  hash1n0  13776  s1nz  13955  isumltss  15197  0subg  18298  pmtrprfvalrn  18610  gsumxp  19090  lsssn0  19713  frlmip  20916  t1connperf  22038  dissnlocfin  22131  isufil2  22510  cnextf  22668  ustuqtop1  22844  rrxip  23987  dveq0  24591  wwlksnext  27665  clwwlknon1sn  27873  esumnul  31302  bnj970  32214  noxp1o  33165  bdayfo  33177  noetalem3  33214  noetalem4  33215  scutun12  33266  filnetlem4  33724  bj-0nelsngl  34278  bj-2upln1upl  34331  dibn0  38283  diophrw  39349  dfac11  39655