Theorem snnz 4672

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

Syntax hints:   ∈ wcel 2111   ≠ wne 2987  Vcvv 3441  ∅c0 4243  {csn 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-dif 3884  df-nul 4244  df-sn 4526

This theorem is referenced by:  snsssn  4732  0nep0  5223  notzfaus  5227  notzfausOLD  5228  nnullss  5319  snopeqop  5361  opthwiener  5369  fparlem3  7792  fparlem4  7793  1n0  8102  fodomr  8652  mapdom3  8673  ssfii  8867  marypha1lem  8881  djuexb  9322  fseqdom  9437  dfac5lem3  9536  isfin1-3  9797  axcc2lem  9847  axdc4lem  9866  fpwwe2lem13  10053  hash1n0  13778  s1nz  13952  isumltss  15195  0subg  18296  pmtrprfvalrn  18608  gsumxp  19089  lsssn0  19712  frlmip  20467  t1connperf  22041  dissnlocfin  22134  isufil2  22513  cnextf  22671  ustuqtop1  22847  rrxip  23994  dveq0  24603  wwlksnext  27679  clwwlknon1sn  27885  esumnul  31417  bnj970  32329  noxp1o  33283  bdayfo  33295  noetalem3  33332  noetalem4  33333  scutun12  33384  filnetlem4  33842  bj-0nelsngl  34407  bj-2upln1upl  34460  dibn0  38449  diophrw  39700  dfac11  40006