![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sssn | Structured version Visualization version GIF version |
Description: The subsets of a singleton. (Contributed by NM, 24-Apr-2004.) |
Ref | Expression |
---|---|
sssn | ⊢ (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵})) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neq0 4069 | . . . . . . 7 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | |
2 | ssel 3734 | . . . . . . . . . . 11 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → 𝑥 ∈ {𝐵})) | |
3 | elsni 4334 | . . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝐵} → 𝑥 = 𝐵) | |
4 | 2, 3 | syl6 35 | . . . . . . . . . 10 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → 𝑥 = 𝐵)) |
5 | eleq1 2823 | . . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴)) | |
6 | 4, 5 | syl6 35 | . . . . . . . . 9 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴))) |
7 | 6 | ibd 258 | . . . . . . . 8 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐴)) |
8 | 7 | exlimdv 2006 | . . . . . . 7 ⊢ (𝐴 ⊆ {𝐵} → (∃𝑥 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐴)) |
9 | 1, 8 | syl5bi 232 | . . . . . 6 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → 𝐵 ∈ 𝐴)) |
10 | snssi 4480 | . . . . . 6 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴) | |
11 | 9, 10 | syl6 35 | . . . . 5 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → {𝐵} ⊆ 𝐴)) |
12 | 11 | anc2li 581 | . . . 4 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → (𝐴 ⊆ {𝐵} ∧ {𝐵} ⊆ 𝐴))) |
13 | eqss 3755 | . . . 4 ⊢ (𝐴 = {𝐵} ↔ (𝐴 ⊆ {𝐵} ∧ {𝐵} ⊆ 𝐴)) | |
14 | 12, 13 | syl6ibr 242 | . . 3 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → 𝐴 = {𝐵})) |
15 | 14 | orrd 392 | . 2 ⊢ (𝐴 ⊆ {𝐵} → (𝐴 = ∅ ∨ 𝐴 = {𝐵})) |
16 | 0ss 4111 | . . . 4 ⊢ ∅ ⊆ {𝐵} | |
17 | sseq1 3763 | . . . 4 ⊢ (𝐴 = ∅ → (𝐴 ⊆ {𝐵} ↔ ∅ ⊆ {𝐵})) | |
18 | 16, 17 | mpbiri 248 | . . 3 ⊢ (𝐴 = ∅ → 𝐴 ⊆ {𝐵}) |
19 | eqimss 3794 | . . 3 ⊢ (𝐴 = {𝐵} → 𝐴 ⊆ {𝐵}) | |
20 | 18, 19 | jaoi 393 | . 2 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) → 𝐴 ⊆ {𝐵}) |
21 | 15, 20 | impbii 199 | 1 ⊢ (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵})) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 ∨ wo 382 ∧ wa 383 = wceq 1628 ∃wex 1849 ∈ wcel 2135 ⊆ wss 3711 ∅c0 4054 {csn 4317 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1867 ax-4 1882 ax-5 1984 ax-6 2050 ax-7 2086 ax-9 2144 ax-10 2164 ax-11 2179 ax-12 2192 ax-13 2387 ax-ext 2736 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1631 df-ex 1850 df-nf 1855 df-sb 2043 df-clab 2743 df-cleq 2749 df-clel 2752 df-nfc 2887 df-v 3338 df-dif 3714 df-in 3718 df-ss 3725 df-nul 4055 df-sn 4318 |
This theorem is referenced by: eqsn 4502 eqsnOLD 4503 snsssn 4513 pwsn 4576 frsn 5342 foconst 6283 fin1a2lem12 9421 fpwwe2lem13 9652 gsumval2 17477 0top 20985 minveclem4a 23397 uvtx01vtx 26496 uvtxa01vtx0OLD 26498 locfinref 30213 ordcmp 32748 bj-snmoore 33370 uneqsn 38819 |
Copyright terms: Public domain | W3C validator |