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. 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 | velsn 4141 | . . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
2 | 1 | imbi1i 338 | . . 3 ⊢ ((𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ (𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
3 | 2 | albii 1737 | . 2 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
4 | dfss2 3557 | . 2 ⊢ ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵)) | |
5 | snss.1 | . . 3 ⊢ 𝐴 ∈ V | |
6 | 5 | clel2 3309 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
7 | 3, 4, 6 | 3bitr4ri 292 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∀wal 1473 = wceq 1475 ∈ wcel 1977 Vcvv 3173 ⊆ wss 3540 {csn 4125 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-in 3547 df-ss 3554 df-sn 4126 |
This theorem is referenced by: snssg 4268 prssOLD 4292 tpss 4308 snelpw 4840 sspwb 4844 nnullss 4857 exss 4858 pwssun 4944 relsn 5146 fvimacnvi 6239 fvimacnv 6240 fvimacnvALT 6244 fnressn 6330 limensuci 8021 domunfican 8118 finsschain 8156 epfrs 8490 tc2 8501 tcsni 8502 cda1dif 8881 fpwwe2lem13 9343 wunfi 9422 uniwun 9441 un0mulcl 11204 nn0ssz 11275 xrinfmss 12012 hashbclem 13093 hashf1lem1 13096 hashf1lem2 13097 fsum2dlem 14343 fsumabs 14374 fsumrlim 14384 fsumo1 14385 fsumiun 14394 incexclem 14407 fprod2dlem 14549 lcmfunsnlem 15192 lcmfun 15196 coprmprod 15213 coprmproddvdslem 15214 ramcl2 15558 0ram 15562 strfv 15735 imasaddfnlem 16011 imasaddvallem 16012 acsfn1 16145 drsdirfi 16761 sylow2a 17857 gsumpt 18184 dprdfadd 18242 ablfac1eulem 18294 pgpfaclem1 18303 rsp1 19045 mplcoe1 19286 mplcoe5 19289 mdetunilem9 20245 opnnei 20734 iscnp4 20877 cnpnei 20878 hausnei2 20967 fiuncmp 21017 llycmpkgen2 21163 1stckgen 21167 ptbasfi 21194 xkoccn 21232 xkoptsub 21267 ptcmpfi 21426 cnextcn 21681 tsmsid 21753 ustuqtop3 21857 utopreg 21866 prdsdsf 21982 prdsmet 21985 prdsbl 22106 fsumcn 22481 itgfsum 23399 dvmptfsum 23542 elply2 23756 elplyd 23762 ply1term 23764 ply0 23768 plymullem 23776 jensenlem1 24513 jensenlem2 24514 frisusgranb 26524 h1de2bi 27797 spansni 27800 gsumle 29110 gsumvsca1 29113 gsumvsca2 29114 ordtconlem1 29298 cntnevol 29618 eulerpartgbij 29761 cvmlift2lem1 30538 cvmlift2lem12 30550 dfon2lem7 30938 bj-tagss 32161 lindsenlbs 32574 matunitlindflem1 32575 divrngidl 32997 isfldidl 33037 ispridlc 33039 pclfinclN 34254 osumcllem10N 34269 pexmidlem7N 34280 acsfn1p 36788 clsk1indlem4 37362 clsk1indlem1 37363 fourierdlem62 39061 frcond3 41440 |
Copyright terms: Public domain | W3C validator |