MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snnz Structured version   Visualization version   GIF version

Theorem snnz 4742
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
StepHypRef Expression
1 snnz.1 . 2 𝐴 ∈ V
2 snnzg 4740 . 2 (𝐴 ∈ V → {𝐴} ≠ ∅)
31, 2ax-mp 5 1 {𝐴} ≠ ∅
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  wne 2944  Vcvv 3448  c0 4287  {csn 4591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-dif 3918  df-nul 4288  df-sn 4592
This theorem is referenced by:  snsssn  4804  0nep0  5318  notzfaus  5323  nnullss  5424  snopeqop  5468  opthwiener  5476  fparlem3  8051  fparlem4  8052  1n0  8439  fodomr  9079  mapdom3  9100  ssfii  9362  marypha1lem  9376  djuexb  9852  fseqdom  9969  dfac5lem3  10068  isfin1-3  10329  axcc2lem  10379  axdc4lem  10398  fpwwe2lem12  10585  hash1n0  14328  s1nz  14502  isumltss  15740  0subgOLD  18961  pmtrprfvalrn  19277  gsumxp  19760  lsssn0  20424  frlmip  21200  t1connperf  22803  dissnlocfin  22896  isufil2  23275  cnextf  23433  ustuqtop1  23609  rrxip  24770  dveq0  25380  noxp1o  27027  bdayfo  27041  noetasuplem2  27098  noetasuplem4  27100  noetainflem2  27102  noetainflem4  27104  scutun12  27171  cuteq0  27193  cofcut1  27261  sleadd1  27320  addsunif  27332  addsasslem1  27333  addsasslem2  27334  negscut2  27360  wwlksnext  28880  clwwlknon1sn  29086  esumnul  32687  bnj970  33599  filnetlem4  34882  bj-0nelsngl  35471  bj-2upln1upl  35524  dibn0  39645  diophrw  41111  dfac11  41418
  Copyright terms: Public domain W3C validator