Theorem snsslVD

Description: Virtual deduction proof of snssl . (Contributed by Alan Sare, 25-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	snsslVD.1	|- A e. _V
Assertion	snsslVD	|- ( { A } C_ B -> A e. B )

Proof

Step	Hyp	Ref	Expression
1		snsslVD.1	|- A e. _V
2		idn1	|- (. { A } C_ B ->. { A } C_ B ).
3	1	snid	|- A e. { A }
4		ssel2	|- ( ( { A } C_ B /\ A e. { A } ) -> A e. B )
5	2 3 4	e10an	|- (. { A } C_ B ->. A e. B ).
6	5	in1	|- ( { A } C_ B -> A e. B )