Theorem snnz 4527

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

Syntax hints:   ∈ wcel 2166   ≠ wne 2998  Vcvv 3413  ∅c0 4143  {csn 4396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2802

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ne 2999  df-v 3415  df-dif 3800  df-nul 4144  df-sn 4397

This theorem is referenced by:  snsssn  4587  0nep0  5057  notzfaus  5061  nnullss  5150  snopeqop  5190  opthwiener  5199  fparlem3  7542  fparlem4  7543  1n0  7841  fodomr  8379  mapdom3  8400  ssfii  8593  marypha1lem  8607  fseqdom  9161  dfac5lem3  9260  isfin1-3  9522  axcc2lem  9572  axdc4lem  9591  fpwwe2lem13  9778  hash1n0  13497  s1nz  13666  isumltss  14953  0subg  17969  pmtrprfvalrn  18257  gsumxp  18727  lsssn0  19303  frlmip  20483  t1connperf  21609  dissnlocfin  21702  isufil2  22081  cnextf  22239  ustuqtop1  22414  rrxip  23557  dveq0  24161  wwlksnext  27203  clwwlknon1sn  27473  esumnul  30654  bnj970  31562  noxp1o  32354  bdayfo  32366  noetalem3  32403  noetalem4  32404  scutun12  32455  filnetlem4  32913  bj-0nelsngl  33480  bj-2upln1upl  33533  dibn0  37227  diophrw  38165  dfac11  38474