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 4593 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) | |
2 | 1 | ne0d 4301 | 1 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2110 ≠ wne 3016 ∅c0 4291 {csn 4561 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-dif 3939 df-nul 4292 df-sn 4562 |
This theorem is referenced by: snnz 4705 0nelop 5379 frirr 5527 frsn 5634 omsucne 7592 1stconst 7789 2ndconst 7790 fczsupp0 7853 hashge3el3dif 13838 pwsbas 16754 pwsle 16759 trnei 22494 uffix 22523 neiflim 22576 hausflim 22583 flimcf 22584 flimclslem 22586 cnpflf2 22602 cnpflf 22603 fclsfnflim 22629 ustneism 22826 ustuqtop5 22848 neipcfilu 22899 dv11cn 24592 cosnop 30425 noextendseq 33169 scutbdaylt 33271 elpaddat 36934 elpadd2at 36936 mnuprdlem1 40601 snn0d 41342 ovnovollem3 42933 |
Copyright terms: Public domain | W3C validator |