Theorem sssn 1852

Description: The only subsets of a singleton are the singleton and the empty set.

Assertion

Ref	Expression
sssn	⊢ (A ⊆ {B} ↔ (A = ∅ ∨ A = {B}))

Proof of Theorem sssn

Step	Hyp	Ref	Expression
1		ssel 1502	. . . . . . . . . . 11 ⊢ (A ⊆ {B} → (x ∈ A → x ∈ {B}))
2		elsni 1827	. . . . . . . . . . 11 ⊢ (x ∈ {B} → x = B)
3	1, 2	syl6 23	. . . . . . . . . 10 ⊢ (A ⊆ {B} → (x ∈ A → x = B))
4		eleq1 1149	. . . . . . . . . 10 ⊢ (x = B → (x ∈ A ↔ B ∈ A))
5	3, 4	syl6 23	. . . . . . . . 9 ⊢ (A ⊆ {B} → (x ∈ A → (x ∈ A ↔ B ∈ A)))
6	5	ibd 451	. . . . . . . 8 ⊢ (A ⊆ {B} → (x ∈ A → B ∈ A))
7	6	19.23adv 954	. . . . . . 7 ⊢ (A ⊆ {B} → (∃x x ∈ A → B ∈ A))
8		n0 1714	. . . . . . 7 ⊢ (¬ A = ∅ ↔ ∃x x ∈ A)
9	7, 8	syl5ib 181	. . . . . 6 ⊢ (A ⊆ {B} → (¬ A = ∅ → B ∈ A))
10		snssi 1851	. . . . . 6 ⊢ (B ∈ A → {B} ⊆ A)
11	9, 10	syl6 23	. . . . 5 ⊢ (A ⊆ {B} → (¬ A = ∅ → {B} ⊆ A))
12	11	anc2li 250	. . . 4 ⊢ (A ⊆ {B} → (¬ A = ∅ → (A ⊆ {B} ∧ {B} ⊆ A)))
13		eqss 1516	. . . 4 ⊢ (A = {B} ↔ (A ⊆ {B} ∧ {B} ⊆ A))
14	12, 13	syl6ibr 186	. . 3 ⊢ (A ⊆ {B} → (¬ A = ∅ → A = {B}))
15	14	orrd 203	. 2 ⊢ (A ⊆ {B} → (A = ∅ ∨ A = {B}))
16		0ss 1725	. . . 4 ⊢ ∅ ⊆ {B}
17		sseq1 1521	. . . 4 ⊢ (A = ∅ → (A ⊆ {B} ↔ ∅ ⊆ {B}))
18	16, 17	mpbiri 169	. . 3 ⊢ (A = ∅ → A ⊆ {B})
19		eqimss 1548	. . 3 ⊢ (A = {B} → A ⊆ {B})
20	18, 19	jaoi 275	. 2 ⊢ ((A = ∅ ∨ A = {B}) → A ⊆ {B})
21	15, 20	impbi 139	1 ⊢ (A ⊆ {B} ↔ (A = ∅ ∨ A = {B}))

Syntax hints:  ¬ wn 1   ↔ wb 127   ∨ wo 195   ∧ wa 196  ∃wex 678   = wceq 1091   ∈ wcel 1092   ⊆ wss 1487  ∅c0 1707  {csn 1808

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-sn 1811  df-pr 1812

metamath.org