![]() |
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 4780 | . 2 ⊢ (𝐴 ∈ V → {𝐴} ≠ ∅) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ {𝐴} ≠ ∅ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2098 ≠ wne 2929 Vcvv 3461 ∅c0 4322 {csn 4630 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ne 2930 df-dif 3947 df-nul 4323 df-sn 4631 |
This theorem is referenced by: snsssn 4844 0nep0 5358 notzfaus 5363 nnullss 5464 snopeqop 5508 opthwiener 5516 fparlem3 8119 fparlem4 8120 1n0 8509 fodomr 9153 mapdom3 9174 ssfii 9444 marypha1lem 9458 djuexb 9934 fseqdom 10051 dfac5lem3 10150 isfin1-3 10411 axcc2lem 10461 axdc4lem 10480 fpwwe2lem12 10667 hash1n0 14416 s1nz 14593 isumltss 15830 0subgOLD 19115 pmtrprfvalrn 19455 gsumxp 19943 lsssn0 20844 pzriprnglem4 21427 frlmip 21729 t1connperf 23384 dissnlocfin 23477 isufil2 23856 cnextf 24014 ustuqtop1 24190 rrxip 25362 dveq0 25977 noxp1o 27642 bdayfo 27656 noetasuplem2 27713 noetasuplem4 27715 noetainflem2 27717 noetainflem4 27719 scutun12 27789 cuteq0 27811 cuteq1 27812 cofcut1 27886 addscut2 27942 sleadd1 27952 addsuniflem 27964 addsasslem1 27966 addsasslem2 27967 negscut2 27998 mulscut2 28083 wwlksnext 29776 clwwlknon1sn 29982 esumnul 33798 bnj970 34709 filnetlem4 35996 bj-0nelsngl 36581 bj-2upln1upl 36634 dibn0 40756 diophrw 42321 dfac11 42628 |
Copyright terms: Public domain | W3C validator |