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	⊢ 𝐴 ∈ V
Assertion	snsslVD	⊢ ( { 𝐴 } ⊆ 𝐵 → 𝐴 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		snsslVD.1	⊢ 𝐴 ∈ V
2		idn1	⊢ (    { 𝐴 } ⊆ 𝐵    ▶    { 𝐴 } ⊆ 𝐵    )
3	1	snid	⊢ 𝐴 ∈ { 𝐴 }
4		ssel2	⊢ ( ( { 𝐴 } ⊆ 𝐵 ∧ 𝐴 ∈ { 𝐴 } ) → 𝐴 ∈ 𝐵 )
5	2 3 4	e10an	⊢ (    { 𝐴 } ⊆ 𝐵    ▶    𝐴 ∈ 𝐵    )
6	5	in1	⊢ ( { 𝐴 } ⊆ 𝐵 → 𝐴 ∈ 𝐵 )