![]() |
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 4346 | . . . . . . 7 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | |
2 | ssel 3976 | . . . . . . . . . . 11 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → 𝑥 ∈ {𝐵})) | |
3 | elsni 4646 | . . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝐵} → 𝑥 = 𝐵) | |
4 | 2, 3 | syl6 35 | . . . . . . . . . 10 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → 𝑥 = 𝐵)) |
5 | eleq1 2822 | . . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴)) | |
6 | 4, 5 | syl6 35 | . . . . . . . . 9 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴))) |
7 | 6 | ibd 269 | . . . . . . . 8 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐴)) |
8 | 7 | exlimdv 1937 | . . . . . . 7 ⊢ (𝐴 ⊆ {𝐵} → (∃𝑥 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐴)) |
9 | 1, 8 | biimtrid 241 | . . . . . 6 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → 𝐵 ∈ 𝐴)) |
10 | snssi 4812 | . . . . . 6 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴) | |
11 | 9, 10 | syl6 35 | . . . . 5 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → {𝐵} ⊆ 𝐴)) |
12 | 11 | anc2li 557 | . . . 4 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → (𝐴 ⊆ {𝐵} ∧ {𝐵} ⊆ 𝐴))) |
13 | eqss 3998 | . . . 4 ⊢ (𝐴 = {𝐵} ↔ (𝐴 ⊆ {𝐵} ∧ {𝐵} ⊆ 𝐴)) | |
14 | 12, 13 | imbitrrdi 251 | . . 3 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → 𝐴 = {𝐵})) |
15 | 14 | orrd 862 | . 2 ⊢ (𝐴 ⊆ {𝐵} → (𝐴 = ∅ ∨ 𝐴 = {𝐵})) |
16 | 0ss 4397 | . . . 4 ⊢ ∅ ⊆ {𝐵} | |
17 | sseq1 4008 | . . . 4 ⊢ (𝐴 = ∅ → (𝐴 ⊆ {𝐵} ↔ ∅ ⊆ {𝐵})) | |
18 | 16, 17 | mpbiri 258 | . . 3 ⊢ (𝐴 = ∅ → 𝐴 ⊆ {𝐵}) |
19 | eqimss 4041 | . . 3 ⊢ (𝐴 = {𝐵} → 𝐴 ⊆ {𝐵}) | |
20 | 18, 19 | jaoi 856 | . 2 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) → 𝐴 ⊆ {𝐵}) |
21 | 15, 20 | impbii 208 | 1 ⊢ (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵})) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 397 ∨ wo 846 = wceq 1542 ∃wex 1782 ∈ wcel 2107 ⊆ wss 3949 ∅c0 4323 {csn 4629 |
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 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-dif 3952 df-in 3956 df-ss 3966 df-nul 4324 df-sn 4630 |
This theorem is referenced by: eqsn 4833 snsssn 4843 pwsn 4901 frsn 5764 foconst 6821 fin1a2lem12 10406 fpwwe2lem12 10637 gsumval2 18605 0top 22486 minveclem4a 24947 uvtx01vtx 28654 snsssng 31752 pmtrcnelor 32252 0ringsubrg 32379 lvecdim0 32691 locfinref 32821 ordcmp 35332 bj-snmoore 35994 nlpineqsn 36289 uneqsn 42776 mosssn 47499 mosssn2 47501 mofsssn 47512 |
Copyright terms: Public domain | W3C validator |