Theorem unipwrVD

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

	Ref	Expression
Assertion	unipwrVD	|- A C_ U. ~P A

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2	1	snid	|- x e. { x }
3		idn1	|- (. x e. A ->. x e. A ).
4		snelpwi	|- ( x e. A -> { x } e. ~P A )
5	3 4	e1a	|- (. x e. A ->. { x } e. ~P A ).
6		elunii	|- ( ( x e. { x } /\ { x } e. ~P A ) -> x e. U. ~P A )
7	2 5 6	e01an	|- (. x e. A ->. x e. U. ~P A ).
8	7	in1	|- ( x e. A -> x e. U. ~P A )
9	8	ssriv	|- A C_ U. ~P A