![]() |
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 4347). 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 4347 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∈ wcel 2030 Vcvv 3231 ⊆ wss 3607 {csn 4210 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-in 3614 df-ss 3621 df-sn 4211 |
This theorem is referenced by: snssgOLD 4349 prssOLD 4384 tpss 4400 snelpw 4943 sspwb 4947 nnullss 4960 exss 4961 pwssun 5049 relsnOLD 5260 fvimacnvi 6371 fvimacnv 6372 fvimacnvALT 6376 fnressn 6465 limensuci 8177 domunfican 8274 finsschain 8314 epfrs 8645 tc2 8656 tcsni 8657 cda1dif 9036 fpwwe2lem13 9502 wunfi 9581 uniwun 9600 un0mulcl 11365 nn0ssz 11436 xrinfmss 12178 hashbclem 13274 hashf1lem1 13277 hashf1lem2 13278 fsum2dlem 14545 fsumabs 14577 fsumrlim 14587 fsumo1 14588 fsumiun 14597 incexclem 14612 fprod2dlem 14754 lcmfunsnlem 15401 lcmfun 15405 coprmprod 15422 coprmproddvdslem 15423 ramcl2 15767 0ram 15771 strfv 15954 imasaddfnlem 16235 imasaddvallem 16236 acsfn1 16369 drsdirfi 16985 sylow2a 18080 gsumpt 18407 dprdfadd 18465 ablfac1eulem 18517 pgpfaclem1 18526 rsp1 19272 mplcoe1 19513 mplcoe5 19516 mdetunilem9 20474 opnnei 20972 iscnp4 21115 cnpnei 21116 hausnei2 21205 fiuncmp 21255 llycmpkgen2 21401 1stckgen 21405 ptbasfi 21432 xkoccn 21470 xkoptsub 21505 ptcmpfi 21664 cnextcn 21918 tsmsid 21990 ustuqtop3 22094 utopreg 22103 prdsdsf 22219 prdsmet 22222 prdsbl 22343 fsumcn 22720 itgfsum 23638 dvmptfsum 23783 elply2 23997 elplyd 24003 ply1term 24005 ply0 24009 plymullem 24017 jensenlem1 24758 jensenlem2 24759 frcond3 27249 h1de2bi 28541 spansni 28544 gsumle 29907 gsumvsca1 29910 gsumvsca2 29911 ordtconnlem1 30098 cntnevol 30419 eulerpartgbij 30562 breprexpnat 30840 cvmlift2lem1 31410 cvmlift2lem12 31422 dfon2lem7 31818 bj-tagss 33093 lindsenlbs 33534 matunitlindflem1 33535 divrngidl 33957 isfldidl 33997 ispridlc 33999 pclfinclN 35554 osumcllem10N 35569 pexmidlem7N 35580 acsfn1p 38086 clsk1indlem4 38659 clsk1indlem1 38660 fourierdlem62 40703 |
Copyright terms: Public domain | W3C validator |