Metamath Proof Explorer


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 ABA𝒫B

Proof

Step Hyp Ref Expression
1 snex AV
2 idn1 ABAB
3 snssi ABAB
4 2 3 e1a ABAB
5 elpwg AVA𝒫BAB
6 5 biimprd AVABA𝒫B
7 1 4 6 e01 ABA𝒫B
8 7 in1 ABA𝒫B