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	|- ( A e. B -> { A } e. ~P B )

Proof

Step	Hyp	Ref	Expression
1		snex	|- { A } e. _V
2		idn1	|- (. A e. B ->. A e. B ).
3		snssi	|- ( A e. B -> { A } C_ B )
4	2 3	e1a	|- (. A e. B ->. { A } C_ B ).
5		elpwg	|- ( { A } e. _V -> ( { A } e. ~P B <-> { A } C_ B ) )
6	5	biimprd	|- ( { A } e. _V -> ( { A } C_ B -> { A } e. ~P B ) )
7	1 4 6	e01	|- (. A e. B ->. { A } e. ~P B ).
8	7	in1	|- ( A e. B -> { A } e. ~P B )