| 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 4660 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) | |
| 2 | 1 | ne0d 4342 | 1 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 ≠ wne 2940 ∅c0 4333 {csn 4626 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-dif 3954 df-nul 4334 df-sn 4627 |
| This theorem is referenced by: snn0d 4775 snnz 4776 frirr 5661 frsn 5773 omsucne 7906 1stconst 8125 2ndconst 8126 fczsupp0 8218 hashge3el3dif 14526 pwsbas 17532 pwsle 17537 trnei 23900 uffix 23929 neiflim 23982 flimclslem 23992 fclsfnflim 24035 ustneism 24232 ustuqtop5 24254 dv11cn 26040 noextendseq 27712 scutbdaylt 27863 lltropt 27911 snsssng 32533 cosnop 32704 elpadd2at 39808 onnog 43442 onnobdayg 43443 bdaybndbday 43445 |
| Copyright terms: Public domain | W3C validator |