Theorem snnz 2449

Description: The singleton of a set is not empty.

Hypothesis

Ref	Expression
snnz.1	|- A e. V

Assertion

Ref	Expression
snnz	|- {A} =/= (/)

Proof of Theorem snnz

Step	Hyp	Ref	Expression
1		snnz.1	. . 3 |- A e. V
2	1	snid 2425	. 2 |- A e. {A}
3		ne0i 2276	. 2 |- (A e. {A} -> {A} =/= (/))
4	2, 3	ax-mp 7	1 |- {A} =/= (/)

Syntax hints:   e. wcel 955   =/= wne 1577  Vcvv 1802  (/)c0 2270  {csn 2399

This theorem is referenced by:  snsssn 2469  0nep0 2727  notzfaus 2731  nnullss 2758  opprc1b 2786  opthwiener 2796  frirr 2914  snsn0non 3115  fconst 3643  fvprc 3706  fvopabn 3771  1ne0 4126  map0 4328  fodomr 4463  aceq5lem3 4709  climuz0 7045

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-nul 2271  df-sn 2402  df-pr 2403

Copyright terms: Public domain