Theorem snelpwrVD

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

	Ref	Expression
Assertion	snelpwrVD	⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ∈ 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		snex	⊢ { 𝐴 } ∈ V
2		idn1	⊢ (    𝐴 ∈ 𝐵    ▶    𝐴 ∈ 𝐵    )
3		snssi	⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ⊆ 𝐵 )
4	2 3	e1a	⊢ (    𝐴 ∈ 𝐵    ▶    { 𝐴 } ⊆ 𝐵    )
5		elpwg	⊢ ( { 𝐴 } ∈ V → ( { 𝐴 } ∈ 𝒫 𝐵 ↔ { 𝐴 } ⊆ 𝐵 ) )
6	5	biimprd	⊢ ( { 𝐴 } ∈ V → ( { 𝐴 } ⊆ 𝐵 → { 𝐴 } ∈ 𝒫 𝐵 ) )
7	1 4 6	e01	⊢ (    𝐴 ∈ 𝐵    ▶    { 𝐴 } ∈ 𝒫 𝐵    )
8	7	in1	⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ∈ 𝒫 𝐵 )