Theorem sssn

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

	Ref	Expression
Assertion	sssn	⊢ ( 𝐴 ⊆ { 𝐵 } ↔ ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) )

Proof

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