Theorem snnz 4309

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

Syntax hints:   ∈ wcel 1990   ≠ wne 2794  Vcvv 3200  ∅c0 3915  {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-v 3202  df-dif 3577  df-nul 3916  df-sn 4178

This theorem is referenced by:  snsssn  4372  0nep0  4836  notzfaus  4840  nnullss  4930  opthwiener  4976  fparlem3  7279  fparlem4  7280  1n0  7575  fodomr  8111  mapdom3  8132  ssfii  8325  marypha1lem  8339  fseqdom  8849  dfac5lem3  8948  isfin1-3  9208  axcc2lem  9258  axdc4lem  9277  fpwwe2lem13  9464  hash1n0  13209  s1nz  13386  isumltss  14580  0subg  17619  pmtrprfvalrn  17908  gsumxp  18375  lsssn0  18948  frlmip  20117  t1connperf  21239  dissnlocfin  21332  isufil2  21712  cnextf  21870  ustuqtop1  22045  rrxip  23178  dveq0  23763  wwlksnext  26788  esumnul  30110  bnj970  31017  noxp1o  31816  bdayfo  31828  noetalem3  31865  noetalem4  31866  scutun12  31917  filnetlem4  32376  bj-0nelsngl  32959  bj-2upln1upl  33012  dibn0  36442  diophrw  37322  dfac11  37632