Theorem snssgOLD

Description: Obsolete version of snssgOLD as of 1-Jan-2025. (Contributed by NM, 22-Jul-2001) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	snssgOLD	|- ( 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 ) )