| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > snnz | Structured version Visualization version GIF version | ||
| Description: The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.) |
| Ref | Expression |
|---|---|
| snnz.1 | ⊢ 𝐴 ∈ V |
| Ref | Expression |
|---|---|
| snnz | ⊢ {𝐴} ≠ ∅ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | snnz.1 | . 2 ⊢ 𝐴 ∈ V | |
| 2 | snnzg 4774 | . 2 ⊢ (𝐴 ∈ V → {𝐴} ≠ ∅) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ {𝐴} ≠ ∅ |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 ≠ wne 2940 Vcvv 3480 ∅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: snsssn 4841 0nep0 5358 notzfaus 5363 nnullss 5467 snopeqop 5511 opthwiener 5519 fparlem3 8139 fparlem4 8140 1n0 8526 fodomr 9168 mapdom3 9189 fodomfir 9368 ssfii 9459 marypha1lem 9473 djuexb 9949 fseqdom 10066 dfac5lem3 10165 isfin1-3 10426 axcc2lem 10476 axdc4lem 10495 fpwwe2lem12 10682 hash1n0 14460 s1nz 14645 isumltss 15884 0subgOLD 19170 pmtrprfvalrn 19506 gsumxp 19994 lsssn0 20946 pzriprnglem4 21495 frlmip 21798 t1connperf 23444 dissnlocfin 23537 isufil2 23916 cnextf 24074 ustuqtop1 24250 rrxip 25424 dveq0 26039 noxp1o 27708 bdayfo 27722 noetasuplem2 27779 noetasuplem4 27781 noetainflem2 27783 noetainflem4 27785 scutun12 27855 cuteq0 27877 cuteq1 27878 cofcut1 27954 addscut2 28012 sleadd1 28022 addsuniflem 28034 addsasslem1 28036 addsasslem2 28037 negscut2 28072 mulscut2 28159 wwlksnext 29913 clwwlknon1sn 30119 esumnul 34049 bnj970 34961 filnetlem4 36382 bj-0nelsngl 36972 bj-2upln1upl 37025 dibn0 41155 diophrw 42770 dfac11 43074 fucofvalne 49020 |
| Copyright terms: Public domain | W3C validator |