Theorem pwpwssunieq

Description: The class of sets whose union is equal to a given class is included in the double power class of that class. (Contributed by BJ, 29-Apr-2021)

	Ref	Expression
Assertion	pwpwssunieq	$$⊢\left\{x|\bigcup x=A\right\}\subseteq 𝒫𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		eqimss	$$⊢\bigcup x=A\to \bigcup x\subseteq A$$
2	1	ss2abi	$$⊢\left\{x|\bigcup x=A\right\}\subseteq \left\{x|\bigcup x\subseteq A\right\}$$
3		pwpwab	$$⊢𝒫𝒫A=\left\{x|\bigcup x\subseteq A\right\}$$
4	2 3	sseqtrri	$$⊢\left\{x|\bigcup x=A\right\}\subseteq 𝒫𝒫A$$