| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > snss | Structured version Visualization version GIF version | ||
| Description: The singleton of an element of a class is a subset of the class (inference form of snssg 4783). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.) |
| Ref | Expression |
|---|---|
| snss.1 | ⊢ 𝐴 ∈ V |
| Ref | Expression |
|---|---|
| snss | ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | snss.1 | . 2 ⊢ 𝐴 ∈ V | |
| 2 | snssg 4783 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∈ wcel 2108 Vcvv 3480 ⊆ wss 3951 {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-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-sn 4627 |
| This theorem is referenced by: tpss 4837 sspwb 5454 nnullss 5467 exss 5468 pwssun 5575 fvimacnvi 7072 fvimacnv 7073 fvimacnvALT 7077 fnressn 7178 limensuci 9193 domunfican 9361 finsschain 9399 epfrs 9771 tc2 9782 tcsni 9783 dju1dif 10213 fpwwe2lem12 10682 wunfi 10761 uniwun 10780 un0mulcl 12560 nn0ssz 12636 xrinfmss 13352 hashbclem 14491 hashf1lem1 14494 hashf1lem2 14495 fsum2dlem 15806 fsumabs 15837 fsumrlim 15847 fsumo1 15848 fsumiun 15857 incexclem 15872 fprod2dlem 16016 lcmfunsnlem 16678 lcmfun 16682 coprmprod 16698 coprmproddvdslem 16699 ramcl2 17054 0ram 17058 strfv 17240 imasaddfnlem 17573 imasaddvallem 17574 acsfn1 17704 drsdirfi 18351 sylow2a 19637 gsumpt 19980 dprdfadd 20040 ablfac1eulem 20092 pgpfaclem1 20101 acsfn1p 20800 rsp1 21247 pzriprnglem4 21495 mplcoe1 22055 mplcoe5 22058 mdetunilem9 22626 opnnei 23128 iscnp4 23271 cnpnei 23272 hausnei2 23361 fiuncmp 23412 llycmpkgen2 23558 1stckgen 23562 ptbasfi 23589 xkoccn 23627 xkoptsub 23662 ptcmpfi 23821 cnextcn 24075 tsmsid 24148 ustuqtop3 24252 utopreg 24261 prdsdsf 24377 prdsmet 24380 prdsbl 24504 fsumcn 24894 itgfsum 25862 dvmptfsum 26013 elply2 26235 elplyd 26241 ply1term 26243 ply0 26247 plymullem 26255 jensenlem1 27030 jensenlem2 27031 frcond3 30288 h1de2bi 31573 spansni 31576 gsumle 33101 gsumvsca1 33232 gsumvsca2 33233 1fldgenq 33324 unitprodclb 33417 mxidlirredi 33499 extdg1id 33716 ordtconnlem1 33923 cntnevol 34229 eulerpartgbij 34374 breprexpnat 34649 cvmlift2lem1 35307 cvmlift2lem12 35319 dfon2lem7 35790 bj-tagss 36981 lindsenlbs 37622 matunitlindflem1 37623 divrngidl 38035 isfldidl 38075 ispridlc 38077 pclfinclN 39952 osumcllem10N 39967 pexmidlem7N 39978 clsk1indlem4 44057 clsk1indlem1 44058 fourierdlem62 46183 |
| Copyright terms: Public domain | W3C validator |