![]() |
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 4592). 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 4592 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∈ wcel 2050 Vcvv 3415 ⊆ wss 3831 {csn 4442 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-v 3417 df-in 3838 df-ss 3845 df-sn 4443 |
This theorem is referenced by: tpss 4643 snelpw 5195 sspwb 5199 nnullss 5212 exss 5213 pwssun 5309 fvimacnvi 6649 fvimacnv 6650 fvimacnvALT 6654 fnressn 6745 limensuci 8491 domunfican 8588 finsschain 8628 epfrs 8969 tc2 8980 tcsni 8981 dju1dif 9398 fpwwe2lem13 9864 wunfi 9943 uniwun 9962 un0mulcl 11746 nn0ssz 11819 xrinfmss 12522 hashbclem 13626 hashf1lem1 13629 hashf1lem2 13630 fsum2dlem 14988 fsumabs 15019 fsumrlim 15029 fsumo1 15030 fsumiun 15039 incexclem 15054 fprod2dlem 15197 lcmfunsnlem 15844 lcmfun 15848 coprmprod 15864 coprmproddvdslem 15865 ramcl2 16211 0ram 16215 strfv 16390 imasaddfnlem 16660 imasaddvallem 16661 acsfn1 16793 drsdirfi 17409 sylow2a 18508 gsumpt 18838 dprdfadd 18895 ablfac1eulem 18947 pgpfaclem1 18956 acsfn1p 19303 rsp1 19721 mplcoe1 19962 mplcoe5 19965 mdetunilem9 20936 opnnei 21435 iscnp4 21578 cnpnei 21579 hausnei2 21668 fiuncmp 21719 llycmpkgen2 21865 1stckgen 21869 ptbasfi 21896 xkoccn 21934 xkoptsub 21969 ptcmpfi 22128 cnextcn 22382 tsmsid 22454 ustuqtop3 22558 utopreg 22567 prdsdsf 22683 prdsmet 22686 prdsbl 22807 fsumcn 23184 itgfsum 24133 dvmptfsum 24278 elply2 24492 elplyd 24498 ply1term 24500 ply0 24504 plymullem 24512 jensenlem1 25269 jensenlem2 25270 frcond3 27806 h1de2bi 29115 spansni 29118 gsumle 30522 gsumvsca1 30525 gsumvsca2 30526 extdg1id 30682 ordtconnlem1 30811 cntnevol 31132 eulerpartgbij 31275 breprexpnat 31553 cvmlift2lem1 32134 cvmlift2lem12 32146 dfon2lem7 32554 bj-tagss 33810 lindsenlbs 34328 matunitlindflem1 34329 divrngidl 34748 isfldidl 34788 ispridlc 34790 pclfinclN 36531 osumcllem10N 36546 pexmidlem7N 36557 clsk1indlem4 39757 clsk1indlem1 39758 fourierdlem62 41885 |
Copyright terms: Public domain | W3C validator |