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	$$⊢\bigcup 𝒫A=A$$

Proof

Step	Hyp	Ref	Expression
1		eluni	$$⊢x\in \bigcup 𝒫A\leftrightarrow \exists y\left(x\in y\wedge y\in 𝒫A\right)$$
2		elelpwi	$$⊢\left(x\in y\wedge y\in 𝒫A\right)\to x\in A$$
3	2	exlimiv	$$⊢\exists y\left(x\in y\wedge y\in 𝒫A\right)\to x\in A$$
4	1 3	sylbi	$$⊢x\in \bigcup 𝒫A\to x\in A$$
5		vsnid	$$⊢x\in \left\{x\right\}$$
6		snelpwi	$$⊢x\in A\to \left\{x\right\}\in 𝒫A$$
7		elunii	$$⊢\left(x\in \left\{x\right\}\wedge \left\{x\right\}\in 𝒫A\right)\to x\in \bigcup 𝒫A$$
8	5 6 7	sylancr	$$⊢x\in A\to x\in \bigcup 𝒫A$$
9	4 8	impbii	$$⊢x\in \bigcup 𝒫A\leftrightarrow x\in A$$
10	9	eqriv	$$⊢\bigcup 𝒫A=A$$