![]() |
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 4526 | . 2 ⊢ (𝐴 ∈ V → {𝐴} ≠ ∅) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ {𝐴} ≠ ∅ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2166 ≠ wne 2998 Vcvv 3413 ∅c0 4143 {csn 4396 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-ext 2802 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ne 2999 df-v 3415 df-dif 3800 df-nul 4144 df-sn 4397 |
This theorem is referenced by: snsssn 4587 0nep0 5057 notzfaus 5061 nnullss 5150 snopeqop 5190 opthwiener 5199 fparlem3 7542 fparlem4 7543 1n0 7841 fodomr 8379 mapdom3 8400 ssfii 8593 marypha1lem 8607 fseqdom 9161 dfac5lem3 9260 isfin1-3 9522 axcc2lem 9572 axdc4lem 9591 fpwwe2lem13 9778 hash1n0 13497 s1nz 13666 isumltss 14953 0subg 17969 pmtrprfvalrn 18257 gsumxp 18727 lsssn0 19303 frlmip 20483 t1connperf 21609 dissnlocfin 21702 isufil2 22081 cnextf 22239 ustuqtop1 22414 rrxip 23557 dveq0 24161 wwlksnext 27203 clwwlknon1sn 27473 esumnul 30654 bnj970 31562 noxp1o 32354 bdayfo 32366 noetalem3 32403 noetalem4 32404 scutun12 32455 filnetlem4 32913 bj-0nelsngl 33480 bj-2upln1upl 33533 dibn0 37227 diophrw 38165 dfac11 38474 |
Copyright terms: Public domain | W3C validator |