Theorem snnz 4703

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

Syntax hints:   ∈ wcel 2108   ≠ wne 3014  Vcvv 3493  ∅c0 4289  {csn 4559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-dif 3937  df-nul 4290  df-sn 4560

This theorem is referenced by:  snsssn  4764  0nep0  5249  notzfaus  5253  notzfausOLD  5254  nnullss  5345  snopeqop  5387  opthwiener  5395  fparlem3  7801  fparlem4  7802  1n0  8111  fodomr  8660  mapdom3  8681  ssfii  8875  marypha1lem  8889  djuexb  9330  fseqdom  9444  dfac5lem3  9543  isfin1-3  9800  axcc2lem  9850  axdc4lem  9869  fpwwe2lem13  10056  hash1n0  13774  s1nz  13953  isumltss  15195  0subg  18296  pmtrprfvalrn  18608  gsumxp  19088  lsssn0  19711  frlmip  20914  t1connperf  22036  dissnlocfin  22129  isufil2  22508  cnextf  22666  ustuqtop1  22842  rrxip  23985  dveq0  24589  wwlksnext  27663  clwwlknon1sn  27871  esumnul  31300  bnj970  32212  noxp1o  33163  bdayfo  33175  noetalem3  33212  noetalem4  33213  scutun12  33264  filnetlem4  33722  bj-0nelsngl  34276  bj-2upln1upl  34329  dibn0  38281  diophrw  39346  dfac11  39652