Theorem snnz 4743

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

Syntax hints:   ∈ wcel 2143   ≠ wne 2958  Vcvv 3455  ∅c0 4287  {csn 4590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-dif 3909  df-nul 4288  df-sn 4591

This theorem is referenced by:  snsssn  4807  0nep0  5330  notsep  5336  nnullss  5445  snopeqop  5491  opthwiener  5499  fparlem3  8110  fparlem4  8111  1n0OLD  8474  fodomr  9117  mapdom3  9138  fodomfir  9288  ssfii  9380  marypha1lem  9394  djuexb  9896  fseqdom  10011  dfac5lem3  10110  isfin1-3  10371  axcc2lem  10421  axdc4lem  10440  fpwwe2lem12  10628  hash1n0  14460  s1nz  14647  isumltss  15904  pmtrprfvalrn  19559  gsumxp  20047  lsssn0  21050  pzriprnglem4  21615  frlmip  21909  t1connperf  23574  dissnlocfin  23667  isufil2  24046  cnextf  24204  ustuqtop1  24379  rrxip  25530  dveq0  26140  noxp1o  27808  bdayfo  27822  noetasuplem2  27879  noetasuplem4  27881  noetainflem2  27883  noetainflem4  27885  cutsun12  27964  cuteq0  27989  cuteq1  27991  cofcut1  28094  addcuts2  28153  leadds1  28163  addsuniflem  28175  addsasslem1  28177  addsasslem2  28178  negcut2  28214  mulcut2  28307  wwlksnext  30223  clwwlknon1sn  30432  esumnul  34419  bnj970  35316  filnetlem4  36873  bj-0nelsngl  37588  bj-2upln1upl  37641  dibn0  41908  diophrw  43473  dfac11  43772  fucofvalne  50086