Theorem snssiALTVD

Description: Virtual deduction proof of snssiALT . (Contributed by Alan Sare, 11-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	snssiALTVD	⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dfss2	⊢ ( { 𝐴 } ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 ) )
2		idn1	⊢ (    𝐴 ∈ 𝐵    ▶    𝐴 ∈ 𝐵    )
3		idn2	⊢ (    𝐴 ∈ 𝐵    ,    𝑥 ∈ { 𝐴 }    ▶    𝑥 ∈ { 𝐴 }    )
4		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
5	3 4	e2bi	⊢ (    𝐴 ∈ 𝐵    ,    𝑥 ∈ { 𝐴 }    ▶    𝑥 = 𝐴    )
6		eleq1a	⊢ ( 𝐴 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) )
7	2 5 6	e12	⊢ (    𝐴 ∈ 𝐵    ,    𝑥 ∈ { 𝐴 }    ▶    𝑥 ∈ 𝐵    )
8	7	in2	⊢ (    𝐴 ∈ 𝐵    ▶    ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 )    )
9	8	gen11	⊢ (    𝐴 ∈ 𝐵    ▶    ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 )    )
10		biimpr	⊢ ( ( { 𝐴 } ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 ) ) → ( ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 ) → { 𝐴 } ⊆ 𝐵 ) )
11	1 9 10	e01	⊢ (    𝐴 ∈ 𝐵    ▶    { 𝐴 } ⊆ 𝐵    )
12	11	in1	⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ⊆ 𝐵 )