![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > snss | Structured version Visualization version Unicode version |
Description: The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
snss.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
snss |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elsn 3994 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | imbi1i 331 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | albii 1702 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | dfss2 3433 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | snss.1 |
. . 3
![]() ![]() ![]() ![]() | |
6 | 5 | clel2 3187 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 3, 4, 6 | 3bitr4ri 286 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-v 3059 df-in 3423 df-ss 3430 df-sn 3981 |
This theorem is referenced by: snssg 4118 prss 4139 tpss 4150 snelpw 4663 sspwb 4666 nnullss 4679 exss 4680 pwssun 4762 relsn 4960 fvimacnvi 6024 fvimacnv 6025 fvimacnvALT 6029 fnressn 6105 limensuci 7779 domunfican 7875 finsschain 7912 epfrs 8246 tc2 8257 tcsni 8258 cda1dif 8637 fpwwe2lem13 9098 wunfi 9177 uniwun 9196 un0mulcl 10938 nn0ssz 10992 xrinfmss 11629 hashbclem 12654 hashf1lem1 12657 hashf1lem2 12658 fsum2dlem 13886 fsumabs 13916 fsumrlim 13926 fsumo1 13927 fsumiun 13936 incexclem 13949 fprod2dlem 14089 lcmfunsnlem 14669 lcmfun 14673 coprmprod 14733 coprmproddvdslem 14734 ramcl2 15028 ramcl2OLD 15029 0ram 15033 strfv 15212 imasaddfnlem 15489 imasaddvallem 15490 acsfn1 15622 drsdirfi 16238 sylow2a 17326 gsumpt 17649 dprdfadd 17708 ablfac1eulem 17760 pgpfaclem1 17769 rsp1 18503 mplcoe1 18744 mplcoe5 18747 mdetunilem9 19700 opnnei 20191 iscnp4 20334 cnpnei 20335 hausnei2 20424 fiuncmp 20474 llycmpkgen2 20620 1stckgen 20624 ptbasfi 20651 xkoccn 20689 xkoptsub 20724 ptcmpfi 20883 cnextcn 21137 tsmsid 21209 ustuqtop3 21313 utopreg 21322 prdsdsf 21437 prdsmet 21440 prdsbl 21561 fsumcn 21957 itgfsum 22840 dvmptfsum 22983 elply2 23206 elplyd 23212 ply1term 23214 ply0 23218 plymullem 23226 jensenlem1 23968 jensenlem2 23969 frisusgranb 25781 h1de2bi 27263 spansni 27266 gsumle 28593 gsumvsca1 28596 gsumvsca2 28597 ordtconlem1 28781 esum2dlem 28964 cntnevol 29101 oms0OLD 29179 eulerpartgbij 29255 cvmlift2lem1 30075 cvmlift2lem12 30087 dfon2lem7 30485 bj-tagss 31620 divrngidl 32307 isfldidl 32347 ispridlc 32349 pclfinclN 33561 osumcllem10N 33576 pexmidlem7N 33587 acsfn1p 36111 fourierdlem62 38133 |
Copyright terms: Public domain | W3C validator |