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 4711). 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 4711 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∈ wcel 2105 Vcvv 3495 ⊆ wss 3935 {csn 4559 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3497 df-in 3942 df-ss 3951 df-sn 4560 |
This theorem is referenced by: tpss 4762 snelpw 5329 sspwb 5333 nnullss 5346 exss 5347 pwssun 5449 fvimacnvi 6815 fvimacnv 6816 fvimacnvALT 6820 fnressn 6913 limensuci 8682 domunfican 8780 finsschain 8820 epfrs 9162 tc2 9173 tcsni 9174 dju1dif 9587 fpwwe2lem13 10053 wunfi 10132 uniwun 10151 un0mulcl 11920 nn0ssz 11992 xrinfmss 12693 hashbclem 13800 hashf1lem1 13803 hashf1lem2 13804 fsum2dlem 15115 fsumabs 15146 fsumrlim 15156 fsumo1 15157 fsumiun 15166 incexclem 15181 fprod2dlem 15324 lcmfunsnlem 15975 lcmfun 15979 coprmprod 15995 coprmproddvdslem 15996 ramcl2 16342 0ram 16346 strfv 16521 imasaddfnlem 16791 imasaddvallem 16792 acsfn1 16922 drsdirfi 17538 sylow2a 18675 gsumpt 19013 dprdfadd 19073 ablfac1eulem 19125 pgpfaclem1 19134 acsfn1p 19509 rsp1 19927 mplcoe1 20176 mplcoe5 20179 mdetunilem9 21159 opnnei 21658 iscnp4 21801 cnpnei 21802 hausnei2 21891 fiuncmp 21942 llycmpkgen2 22088 1stckgen 22092 ptbasfi 22119 xkoccn 22157 xkoptsub 22192 ptcmpfi 22351 cnextcn 22605 tsmsid 22677 ustuqtop3 22781 utopreg 22790 prdsdsf 22906 prdsmet 22909 prdsbl 23030 fsumcn 23407 itgfsum 24356 dvmptfsum 24501 elply2 24715 elplyd 24721 ply1term 24723 ply0 24727 plymullem 24735 jensenlem1 25492 jensenlem2 25493 frcond3 27976 h1de2bi 29259 spansni 29262 gsumle 30653 gsumvsca1 30782 gsumvsca2 30783 extdg1id 30953 ordtconnlem1 31067 cntnevol 31387 eulerpartgbij 31530 breprexpnat 31805 cvmlift2lem1 32447 cvmlift2lem12 32459 dfon2lem7 32932 bj-tagss 34190 lindsenlbs 34769 matunitlindflem1 34770 divrngidl 35189 isfldidl 35229 ispridlc 35231 pclfinclN 36968 osumcllem10N 36983 pexmidlem7N 36994 clsk1indlem4 40274 clsk1indlem1 40275 fourierdlem62 42334 |
Copyright terms: Public domain | W3C validator |