Metamath Proof Explorer

Theorem sssn

Description: The subsets of a singleton. (Contributed by NM, 24-Apr-2004)

Ref Expression
Assertion sssn ⊢ A ⊆ B ↔ A = ∅ ∨ A = B

Proof

Step Hyp Ref Expression
1 neq0 ⊢ ¬ A = ∅ ↔ ∃ x x ∈ A
2 ssel ⊢ A ⊆ B → x ∈ A → x ∈ B
3 elsni ⊢ x ∈ B → x = B
4 2 3 syl6 ⊢ A ⊆ B → x ∈ A → x = B
5 eleq1 ⊢ x = B → x ∈ A ↔ B ∈ A
6 4 5 syl6 ⊢ A ⊆ B → x ∈ A → x ∈ A ↔ B ∈ A
7 6 ibd ⊢ A ⊆ B → x ∈ A → B ∈ A
8 7 exlimdv ⊢ A ⊆ B → ∃ x x ∈ A → B ∈ A
9 1 8 biimtrid ⊢ A ⊆ B → ¬ A = ∅ → B ∈ A
10 snssi ⊢ B ∈ A → B ⊆ A
11 9 10 syl6 ⊢ A ⊆ B → ¬ A = ∅ → B ⊆ A
12 11 anc2li ⊢ A ⊆ B → ¬ A = ∅ → A ⊆ B ∧ B ⊆ A
13 eqss ⊢ A = B ↔ A ⊆ B ∧ B ⊆ A
14 12 13 imbitrrdi ⊢ A ⊆ B → ¬ A = ∅ → A = B
15 14 orrd ⊢ A ⊆ B → A = ∅ ∨ A = B
16 0ss ⊢ ∅ ⊆ B
17 sseq1 ⊢ A = ∅ → A ⊆ B ↔ ∅ ⊆ B
18 16 17 mpbiri ⊢ A = ∅ → A ⊆ B
19 eqimss ⊢ A = B → A ⊆ B
20 18 19 jaoi ⊢ A = ∅ ∨ A = B → A ⊆ B
21 15 20 impbii ⊢ A ⊆ B ↔ A = ∅ ∨ A = B