Theorem snnz 4752

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

Syntax hints:   ∈ wcel 2108   ≠ wne 2932  Vcvv 3459  ∅c0 4308  {csn 4601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-dif 3929  df-nul 4309  df-sn 4602

This theorem is referenced by:  snsssn  4817  0nep0  5328  notzfaus  5333  nnullss  5437  snopeqop  5481  opthwiener  5489  fparlem3  8113  fparlem4  8114  1n0  8500  fodomr  9142  mapdom3  9163  fodomfir  9340  ssfii  9431  marypha1lem  9445  djuexb  9923  fseqdom  10040  dfac5lem3  10139  isfin1-3  10400  axcc2lem  10450  axdc4lem  10469  fpwwe2lem12  10656  hash1n0  14439  s1nz  14625  isumltss  15864  0subgOLD  19135  pmtrprfvalrn  19469  gsumxp  19957  lsssn0  20905  pzriprnglem4  21445  frlmip  21738  t1connperf  23374  dissnlocfin  23467  isufil2  23846  cnextf  24004  ustuqtop1  24180  rrxip  25342  dveq0  25957  noxp1o  27627  bdayfo  27641  noetasuplem2  27698  noetasuplem4  27700  noetainflem2  27702  noetainflem4  27704  scutun12  27774  cuteq0  27796  cuteq1  27798  cofcut1  27880  addscut2  27938  sleadd1  27948  addsuniflem  27960  addsasslem1  27962  addsasslem2  27963  negscut2  27998  mulscut2  28088  wwlksnext  29875  clwwlknon1sn  30081  esumnul  34079  bnj970  34978  filnetlem4  36399  bj-0nelsngl  36989  bj-2upln1upl  37042  dibn0  41172  diophrw  42782  dfac11  43086  fucofvalne  49236