Theorem snssg

Description: The singleton of an element of a class is a subset of the class (general form of snss ). Theorem 7.4 of Quine p. 49. (Contributed by NM, 22-Jul-2001)

	Ref	Expression
Assertion	snssg	|- ( A e. V -> ( A e. B <-> { A } C_ B ) )

Proof

Step	Hyp	Ref	Expression
1		velsn	|- ( x e. { A } <-> x = A )
2	1	imbi1i	|- ( ( x e. { A } -> x e. B ) <-> ( x = A -> x e. B ) )
3	2	albii	|- ( A. x ( x e. { A } -> x e. B ) <-> A. x ( x = A -> x e. B ) )
4	3	a1i	|- ( A e. V -> ( A. x ( x e. { A } -> x e. B ) <-> A. x ( x = A -> x e. B ) ) )
5		dfss2	|- ( { A } C_ B <-> A. x ( x e. { A } -> x e. B ) )
6	5	a1i	|- ( A e. V -> ( { A } C_ B <-> A. x ( x e. { A } -> x e. B ) ) )
7		clel2g	|- ( A e. V -> ( A e. B <-> A. x ( x = A -> x e. B ) ) )
8	4 6 7	3bitr4rd	|- ( A e. V -> ( A e. B <-> { A } C_ B ) )