Theorem unipw

Description: A class equals the union of its power class. Exercise 6(a) of Enderton p. 38. (Contributed by NM, 14-Oct-1996) (Proof shortened by Alan Sare, 28-Dec-2008)

	Ref	Expression
Assertion	unipw	|- U. ~P A = A

Proof

Step	Hyp	Ref	Expression
1		eluni	|- ( x e. U. ~P A <-> E. y ( x e. y /\ y e. ~P A ) )
2		elelpwi	|- ( ( x e. y /\ y e. ~P A ) -> x e. A )
3	2	exlimiv	|- ( E. y ( x e. y /\ y e. ~P A ) -> x e. A )
4	1 3	sylbi	|- ( x e. U. ~P A -> x e. A )
5		vsnid	|- x e. { x }
6		snelpwi	|- ( x e. A -> { x } e. ~P A )
7		elunii	|- ( ( x e. { x } /\ { x } e. ~P A ) -> x e. U. ~P A )
8	5 6 7	sylancr	|- ( x e. A -> x e. U. ~P A )
9	4 8	impbii	|- ( x e. U. ~P A <-> x e. A )
10	9	eqriv	|- U. ~P A = A