Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > snnzg | Structured version Visualization version GIF version |
Description: The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.) |
Ref | Expression |
---|---|
snnzg | ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snidg 4550 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) | |
2 | 1 | ne0d 4224 | 1 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2114 ≠ wne 2934 ∅c0 4211 {csn 4516 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-ne 2935 df-dif 3846 df-nul 4212 df-sn 4517 |
This theorem is referenced by: snn0d 4666 snnz 4667 frirr 5502 frsn 5610 omsucne 7619 1stconst 7823 2ndconst 7824 fczsupp0 7890 hashge3el3dif 13940 pwsbas 16865 pwsle 16870 trnei 22645 uffix 22674 neiflim 22727 flimclslem 22737 fclsfnflim 22780 ustneism 22977 ustuqtop5 22999 dv11cn 24755 snsssng 30436 cosnop 30605 noextendseq 33515 scutbdaylt 33657 lltropt 33701 elpadd2at 37465 |
Copyright terms: Public domain | W3C validator |