![]() |
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 4787). 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 4787 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∈ wcel 2105 Vcvv 3473 ⊆ wss 3948 {csn 4628 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-in 3955 df-ss 3965 df-sn 4629 |
This theorem is referenced by: tpss 4838 sspwb 5449 nnullss 5462 exss 5463 pwssun 5571 fvimacnvi 7053 fvimacnv 7054 fvimacnvALT 7058 fnressn 7158 limensuci 9159 domunfican 9326 finsschain 9365 epfrs 9732 tc2 9743 tcsni 9744 dju1dif 10173 fpwwe2lem12 10643 wunfi 10722 uniwun 10741 un0mulcl 12513 nn0ssz 12588 xrinfmss 13296 hashbclem 14418 hashf1lem1 14422 hashf1lem1OLD 14423 hashf1lem2 14424 fsum2dlem 15723 fsumabs 15754 fsumrlim 15764 fsumo1 15765 fsumiun 15774 incexclem 15789 fprod2dlem 15931 lcmfunsnlem 16585 lcmfun 16589 coprmprod 16605 coprmproddvdslem 16606 ramcl2 16956 0ram 16960 strfv 17144 imasaddfnlem 17481 imasaddvallem 17482 acsfn1 17612 drsdirfi 18268 sylow2a 19535 gsumpt 19878 dprdfadd 19938 ablfac1eulem 19990 pgpfaclem1 19999 acsfn1p 20646 rsp1 21087 pzriprnglem4 21344 mplcoe1 21903 mplcoe5 21906 mdetunilem9 22442 opnnei 22944 iscnp4 23087 cnpnei 23088 hausnei2 23177 fiuncmp 23228 llycmpkgen2 23374 1stckgen 23378 ptbasfi 23405 xkoccn 23443 xkoptsub 23478 ptcmpfi 23637 cnextcn 23891 tsmsid 23964 ustuqtop3 24068 utopreg 24077 prdsdsf 24193 prdsmet 24196 prdsbl 24320 fsumcn 24708 itgfsum 25676 dvmptfsum 25827 elply2 26048 elplyd 26054 ply1term 26056 ply0 26060 plymullem 26068 jensenlem1 26832 jensenlem2 26833 frcond3 29955 h1de2bi 31240 spansni 31243 gsumle 32678 gsumvsca1 32807 gsumvsca2 32808 1fldgenq 32848 mxidlirredi 33027 extdg1id 33196 ordtconnlem1 33368 cntnevol 33690 eulerpartgbij 33835 breprexpnat 34110 cvmlift2lem1 34757 cvmlift2lem12 34769 dfon2lem7 35231 bj-tagss 36325 lindsenlbs 36947 matunitlindflem1 36948 divrngidl 37360 isfldidl 37400 ispridlc 37402 pclfinclN 39285 osumcllem10N 39300 pexmidlem7N 39311 clsk1indlem4 43258 clsk1indlem1 43259 fourierdlem62 45343 |
Copyright terms: Public domain | W3C validator |