Theorem pwuni

Description: A class is a subclass of the power class of its union. Exercise 6(b) of Enderton p. 38. (Contributed by NM, 14-Oct-1996)

	Ref	Expression
Assertion	pwuni	$$⊢A\subseteq 𝒫\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		elssuni	$$⊢x\in A\to x\subseteq \bigcup A$$
2		velpw	$$⊢x\in 𝒫\bigcup A\leftrightarrow x\subseteq \bigcup A$$
3	1 2	sylibr	$$⊢x\in A\to x\in 𝒫\bigcup A$$
4	3	ssriv	$$⊢A\subseteq 𝒫\bigcup A$$