![]() |
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 4670 | . 2 ⊢ (𝐴 ∈ V → {𝐴} ≠ ∅) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ {𝐴} ≠ ∅ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2111 ≠ wne 2987 Vcvv 3441 ∅c0 4243 {csn 4525 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-ne 2988 df-dif 3884 df-nul 4244 df-sn 4526 |
This theorem is referenced by: snsssn 4732 0nep0 5223 notzfaus 5227 notzfausOLD 5228 nnullss 5319 snopeqop 5361 opthwiener 5369 fparlem3 7792 fparlem4 7793 1n0 8102 fodomr 8652 mapdom3 8673 ssfii 8867 marypha1lem 8881 djuexb 9322 fseqdom 9437 dfac5lem3 9536 isfin1-3 9797 axcc2lem 9847 axdc4lem 9866 fpwwe2lem13 10053 hash1n0 13778 s1nz 13952 isumltss 15195 0subg 18296 pmtrprfvalrn 18608 gsumxp 19089 lsssn0 19712 frlmip 20467 t1connperf 22041 dissnlocfin 22134 isufil2 22513 cnextf 22671 ustuqtop1 22847 rrxip 23994 dveq0 24603 wwlksnext 27679 clwwlknon1sn 27885 esumnul 31417 bnj970 32329 noxp1o 33283 bdayfo 33295 noetalem3 33332 noetalem4 33333 scutun12 33384 filnetlem4 33842 bj-0nelsngl 34407 bj-2upln1upl 34460 dibn0 38449 diophrw 39700 dfac11 40006 |
Copyright terms: Public domain | W3C validator |