Theorem snssiALT

Description: If a class is an element of another class, then its singleton is a subclass of that other class. Alternate proof of snssi . This theorem was automatically generated from snssiALTVD using a translation program. (Contributed by Alan Sare, 11-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	snssiALT	|- ( A e. B -> { A } C_ B )

Proof

Step	Hyp	Ref	Expression
1		velsn	|- ( x e. { A } <-> x = A )
2		eleq1a	|- ( A e. B -> ( x = A -> x e. B ) )
3	1 2	syl5bi	|- ( A e. B -> ( x e. { A } -> x e. B ) )
4	3	alrimiv	|- ( A e. B -> A. x ( x e. { A } -> x e. B ) )
5		dfss2	|- ( { A } C_ B <-> A. x ( x e. { A } -> x e. B ) )
6	4 5	sylibr	|- ( A e. B -> { A } C_ B )