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 | velsn 4193 | . . . 4 | |
2 | 1 | imbi1i 339 | . . 3 |
3 | 2 | albii 1747 | . 2 |
4 | dfss2 3591 | . 2 | |
5 | snss.1 | . . 3 | |
6 | 5 | clel2 3339 | . 2 |
7 | 3, 4, 6 | 3bitr4ri 293 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wal 1481 wceq 1483 wcel 1990 cvv 3200 wss 3574 csn 4177 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-in 3581 df-ss 3588 df-sn 4178 |
This theorem is referenced by: snssg 4327 prssOLD 4352 tpss 4368 snelpw 4913 sspwb 4917 nnullss 4930 exss 4931 pwssun 5020 relsn 5223 fvimacnvi 6331 fvimacnv 6332 fvimacnvALT 6336 fnressn 6425 limensuci 8136 domunfican 8233 finsschain 8273 epfrs 8607 tc2 8618 tcsni 8619 cda1dif 8998 fpwwe2lem13 9464 wunfi 9543 uniwun 9562 un0mulcl 11327 nn0ssz 11398 xrinfmss 12140 hashbclem 13236 hashf1lem1 13239 hashf1lem2 13240 fsum2dlem 14501 fsumabs 14533 fsumrlim 14543 fsumo1 14544 fsumiun 14553 incexclem 14568 fprod2dlem 14710 lcmfunsnlem 15354 lcmfun 15358 coprmprod 15375 coprmproddvdslem 15376 ramcl2 15720 0ram 15724 strfv 15907 imasaddfnlem 16188 imasaddvallem 16189 acsfn1 16322 drsdirfi 16938 sylow2a 18034 gsumpt 18361 dprdfadd 18419 ablfac1eulem 18471 pgpfaclem1 18480 rsp1 19224 mplcoe1 19465 mplcoe5 19468 mdetunilem9 20426 opnnei 20924 iscnp4 21067 cnpnei 21068 hausnei2 21157 fiuncmp 21207 llycmpkgen2 21353 1stckgen 21357 ptbasfi 21384 xkoccn 21422 xkoptsub 21457 ptcmpfi 21616 cnextcn 21871 tsmsid 21943 ustuqtop3 22047 utopreg 22056 prdsdsf 22172 prdsmet 22175 prdsbl 22296 fsumcn 22673 itgfsum 23593 dvmptfsum 23738 elply2 23952 elplyd 23958 ply1term 23960 ply0 23964 plymullem 23972 jensenlem1 24713 jensenlem2 24714 frcond3 27133 h1de2bi 28413 spansni 28416 gsumle 29779 gsumvsca1 29782 gsumvsca2 29783 ordtconnlem1 29970 cntnevol 30291 eulerpartgbij 30434 breprexpnat 30712 cvmlift2lem1 31284 cvmlift2lem12 31296 dfon2lem7 31694 bj-tagss 32968 lindsenlbs 33404 matunitlindflem1 33405 divrngidl 33827 isfldidl 33867 ispridlc 33869 pclfinclN 35236 osumcllem10N 35251 pexmidlem7N 35262 acsfn1p 37769 clsk1indlem4 38342 clsk1indlem1 38343 fourierdlem62 40385 |
Copyright terms: Public domain | W3C validator |