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 4595 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) | |
2 | 1 | ne0d 4269 | 1 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 ≠ wne 2943 ∅c0 4256 {csn 4561 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ne 2944 df-dif 3890 df-nul 4257 df-sn 4562 |
This theorem is referenced by: snn0d 4711 snnz 4712 frirr 5566 frsn 5674 omsucne 7731 1stconst 7940 2ndconst 7941 fczsupp0 8009 hashge3el3dif 14200 pwsbas 17198 pwsle 17203 trnei 23043 uffix 23072 neiflim 23125 flimclslem 23135 fclsfnflim 23178 ustneism 23375 ustuqtop5 23397 dv11cn 25165 snsssng 30860 cosnop 31028 noextendseq 33870 scutbdaylt 34012 lltropt 34056 elpadd2at 37820 |
Copyright terms: Public domain | W3C validator |