Theorem snnz 4733

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

This proof depends on syntax axioms:   ∈ wcel 2144   ≠ wne 2955  Vcvv 3450  ∅c0 4278  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-dif 4047  df-nul 4279  df-sn 4585

This theorem is used by:  snsssn  4795  0nep0  5318  notsep  5324  nnullss  5429  snopeqop  5477  opthwiener  5486  fparlem3  8127  fparlem4  8128  1n0OLD  8499  fodomr  9150  mapdom3  9171  fodomfir  9322  ssfii  9414  marypha1lem  9428  djuexb  9993  fseqdom  10108  dfac5lem3  10207  isfin1-3  10467  axcc2lem  10517  axdc4lem  10536  fpwwe2lem12  10730  hash1n0  14569  s1nz  14757  isumltss  16022  degenmgmnfn  19141  pmtrprfvalrn  19707  gsumxp  20195  lsssn0  21228  pzriprnglem4  21795  frlmip  22089  t1connperf  23759  dissnlocfin  23853  isufil2  24232  cnextf  24390  ustuqtop1  24565  rrxip  25716  dveq0  26325  noxp1o  28025  bdayfo  28039  noetasuplem2  28096  noetasuplem4  28098  noetainflem2  28100  noetainflem4  28102  cutsun12  28181  cuteq0  28206  cuteq1  28208  cofcut1  28311  addcuts2  28370  leadds1  28380  addsuniflem  28392  addsasslem1  28394  addsasslem2  28395  negcut2  28431  mulcut2  28524  wwlksnext  30487  clwwlknon1sn  30696  esumnul  34726  bnj970  35623  filnetlem4  37261  bj-0nelsngl  37976  bj-2upln1upl  38029  dibn0  42303  diophrw  43863  dfac11  44157  fucofvalne  50540