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 4589 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) | |
2 | 1 | ne0d 4298 | 1 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 ≠ wne 3013 ∅c0 4288 {csn 4557 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ne 3014 df-dif 3936 df-nul 4289 df-sn 4558 |
This theorem is referenced by: snnz 4703 0nelop 5377 frirr 5525 frsn 5632 omsucne 7587 1stconst 7784 2ndconst 7785 fczsupp0 7848 hashge3el3dif 13832 pwsbas 16748 pwsle 16753 trnei 22428 uffix 22457 neiflim 22510 hausflim 22517 flimcf 22518 flimclslem 22520 cnpflf2 22536 cnpflf 22537 fclsfnflim 22563 ustneism 22759 ustuqtop5 22781 neipcfilu 22832 dv11cn 24525 cosnop 30357 noextendseq 33071 scutbdaylt 33173 elpaddat 36820 elpadd2at 36822 mnuprdlem1 40485 snn0d 41226 ovnovollem3 42817 |
Copyright terms: Public domain | W3C validator |