Theorem sssn

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

	Ref	Expression
Assertion	sssn	|- ( A C_ { B } <-> ( A = (/) \/ A = { B } ) )

Proof

Step	Hyp	Ref	Expression
1		neq0	|- ( -. A = (/) <-> E. x x e. A )
2		ssel	|- ( A C_ { B } -> ( x e. A -> x e. { B } ) )
3		elsni	|- ( x e. { B } -> x = B )
4	2 3	syl6	|- ( A C_ { B } -> ( x e. A -> x = B ) )
5		eleq1	|- ( x = B -> ( x e. A <-> B e. A ) )
6	4 5	syl6	|- ( A C_ { B } -> ( x e. A -> ( x e. A <-> B e. A ) ) )
7	6	ibd	|- ( A C_ { B } -> ( x e. A -> B e. A ) )
8	7	exlimdv	|- ( A C_ { B } -> ( E. x x e. A -> B e. A ) )
9	1 8	biimtrid	|- ( A C_ { B } -> ( -. A = (/) -> B e. A ) )
10		snssi	|- ( B e. A -> { B } C_ A )
11	9 10	syl6	|- ( A C_ { B } -> ( -. A = (/) -> { B } C_ A ) )
12	11	anc2li	|- ( A C_ { B } -> ( -. A = (/) -> ( A C_ { B } /\ { B } C_ A ) ) )
13		eqss	|- ( A = { B } <-> ( A C_ { B } /\ { B } C_ A ) )
14	12 13	imbitrrdi	|- ( A C_ { B } -> ( -. A = (/) -> A = { B } ) )
15	14	orrd	|- ( A C_ { B } -> ( A = (/) \/ A = { B } ) )
16		0ss	|- (/) C_ { B }
17		sseq1	|- ( A = (/) -> ( A C_ { B } <-> (/) C_ { B } ) )
18	16 17	mpbiri	|- ( A = (/) -> A C_ { B } )
19		eqimss	|- ( A = { B } -> A C_ { B } )
20	18 19	jaoi	|- ( ( A = (/) \/ A = { B } ) -> A C_ { B } )
21	15 20	impbii	|- ( A C_ { B } <-> ( A = (/) \/ A = { B } ) )