![]() |
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 4749). 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 4749 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∈ wcel 2107 Vcvv 3448 ⊆ wss 3915 {csn 4591 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3450 df-in 3922 df-ss 3932 df-sn 4592 |
This theorem is referenced by: tpss 4800 sspwb 5411 nnullss 5424 exss 5425 pwssun 5533 fvimacnvi 7007 fvimacnv 7008 fvimacnvALT 7012 fnressn 7109 limensuci 9104 domunfican 9271 finsschain 9310 epfrs 9674 tc2 9685 tcsni 9686 dju1dif 10115 fpwwe2lem12 10585 wunfi 10664 uniwun 10683 un0mulcl 12454 nn0ssz 12529 xrinfmss 13236 hashbclem 14356 hashf1lem1 14360 hashf1lem1OLD 14361 hashf1lem2 14362 fsum2dlem 15662 fsumabs 15693 fsumrlim 15703 fsumo1 15704 fsumiun 15713 incexclem 15728 fprod2dlem 15870 lcmfunsnlem 16524 lcmfun 16528 coprmprod 16544 coprmproddvdslem 16545 ramcl2 16895 0ram 16899 strfv 17083 imasaddfnlem 17417 imasaddvallem 17418 acsfn1 17548 drsdirfi 18201 sylow2a 19408 gsumpt 19746 dprdfadd 19806 ablfac1eulem 19858 pgpfaclem1 19867 acsfn1p 20282 rsp1 20710 mplcoe1 21454 mplcoe5 21457 mdetunilem9 21985 opnnei 22487 iscnp4 22630 cnpnei 22631 hausnei2 22720 fiuncmp 22771 llycmpkgen2 22917 1stckgen 22921 ptbasfi 22948 xkoccn 22986 xkoptsub 23021 ptcmpfi 23180 cnextcn 23434 tsmsid 23507 ustuqtop3 23611 utopreg 23620 prdsdsf 23736 prdsmet 23739 prdsbl 23863 fsumcn 24249 itgfsum 25207 dvmptfsum 25355 elply2 25573 elplyd 25579 ply1term 25581 ply0 25585 plymullem 25593 jensenlem1 26352 jensenlem2 26353 frcond3 29255 h1de2bi 30538 spansni 30541 gsumle 31974 gsumvsca1 32103 gsumvsca2 32104 1fldgenq 32129 extdg1id 32392 ordtconnlem1 32545 cntnevol 32867 eulerpartgbij 33012 breprexpnat 33287 cvmlift2lem1 33936 cvmlift2lem12 33948 dfon2lem7 34403 bj-tagss 35480 lindsenlbs 36102 matunitlindflem1 36103 divrngidl 36516 isfldidl 36556 ispridlc 36558 pclfinclN 38442 osumcllem10N 38457 pexmidlem7N 38468 clsk1indlem4 42390 clsk1indlem1 42391 fourierdlem62 44483 |
Copyright terms: Public domain | W3C validator |