Theorem snnz 4735

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

Syntax hints:   ∈ wcel 2114   ≠ wne 2933  Vcvv 3442  ∅c0 4287  {csn 4582

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-dif 3906  df-nul 4288  df-sn 4583

This theorem is referenced by:  snsssn  4799  0nep0  5305  notzfaus  5310  nnullss  5417  snopeqop  5462  opthwiener  5470  fparlem3  8066  fparlem4  8067  1n0  8425  fodomr  9068  mapdom3  9089  fodomfir  9240  ssfii  9334  marypha1lem  9348  djuexb  9833  fseqdom  9948  dfac5lem3  10047  isfin1-3  10308  axcc2lem  10358  axdc4lem  10377  fpwwe2lem12  10565  hash1n0  14356  s1nz  14543  isumltss  15783  pmtrprfvalrn  19429  gsumxp  19917  lsssn0  20911  pzriprnglem4  21451  frlmip  21745  t1connperf  23392  dissnlocfin  23485  isufil2  23864  cnextf  24022  ustuqtop1  24197  rrxip  25358  dveq0  25973  noxp1o  27643  bdayfo  27657  noetasuplem2  27714  noetasuplem4  27716  noetainflem2  27718  noetainflem4  27720  cutsun12  27798  cuteq0  27823  cuteq1  27825  cofcut1  27928  addcuts2  27987  leadds1  27997  addsuniflem  28009  addsasslem1  28011  addsasslem2  28012  negcut2  28048  mulcut2  28141  wwlksnext  29978  clwwlknon1sn  30187  esumnul  34225  bnj970  35122  filnetlem4  36594  bj-0nelsngl  37213  bj-2upln1upl  37266  dibn0  41523  diophrw  43110  dfac11  43413  fucofvalne  49678