Theorem sssn

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

	Ref	Expression
Assertion	sssn	$$⊢A\subseteq \left\{B\right\}\leftrightarrow \left(A=\varnothing \vee A=\left\{B\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		neq0	$$⊢\neg A=\varnothing \leftrightarrow \exists xx\in A$$
2		ssel	$$⊢A\subseteq \left\{B\right\}\to \left(x\in A\to x\in \left\{B\right\}\right)$$
3		elsni	$$⊢x\in \left\{B\right\}\to x=B$$
4	2 3	syl6	$$⊢A\subseteq \left\{B\right\}\to \left(x\in A\to x=B\right)$$
5		eleq1	$$⊢x=B\to \left(x\in A\leftrightarrow B\in A\right)$$
6	4 5	syl6	$$⊢A\subseteq \left\{B\right\}\to \left(x\in A\to \left(x\in A\leftrightarrow B\in A\right)\right)$$
7	6	ibd	$$⊢A\subseteq \left\{B\right\}\to \left(x\in A\to B\in A\right)$$
8	7	exlimdv	$$⊢A\subseteq \left\{B\right\}\to \left(\exists xx\in A\to B\in A\right)$$
9	1 8	biimtrid	$$⊢A\subseteq \left\{B\right\}\to \left(\neg A=\varnothing \to B\in A\right)$$
10		snssi	$$⊢B\in A\to \left\{B\right\}\subseteq A$$
11	9 10	syl6	$$⊢A\subseteq \left\{B\right\}\to \left(\neg A=\varnothing \to \left\{B\right\}\subseteq A\right)$$
12	11	anc2li	$$⊢A\subseteq \left\{B\right\}\to \left(\neg A=\varnothing \to \left(A\subseteq \left\{B\right\}\wedge \left\{B\right\}\subseteq A\right)\right)$$
13		eqss	$$⊢A=\left\{B\right\}\leftrightarrow \left(A\subseteq \left\{B\right\}\wedge \left\{B\right\}\subseteq A\right)$$
14	12 13	imbitrrdi	$$⊢A\subseteq \left\{B\right\}\to \left(\neg A=\varnothing \to A=\left\{B\right\}\right)$$
15	14	orrd	$$⊢A\subseteq \left\{B\right\}\to \left(A=\varnothing \vee A=\left\{B\right\}\right)$$
16		0ss	$$⊢\varnothing \subseteq \left\{B\right\}$$
17		sseq1	$$⊢A=\varnothing \to \left(A\subseteq \left\{B\right\}\leftrightarrow \varnothing \subseteq \left\{B\right\}\right)$$
18	16 17	mpbiri	$$⊢A=\varnothing \to A\subseteq \left\{B\right\}$$
19		eqimss	$$⊢A=\left\{B\right\}\to A\subseteq \left\{B\right\}$$
20	18 19	jaoi	$$⊢\left(A=\varnothing \vee A=\left\{B\right\}\right)\to A\subseteq \left\{B\right\}$$
21	15 20	impbii	$$⊢A\subseteq \left\{B\right\}\leftrightarrow \left(A=\varnothing \vee A=\left\{B\right\}\right)$$