Theorem pwuncl

Description: Power classes are closed under union. (Contributed by AV, 27-Feb-2024)

	Ref	Expression
Assertion	pwuncl	$$⊢\left(A\in 𝒫X\wedge B\in 𝒫X\right)\to A\cup B\in 𝒫X$$

Proof

Step	Hyp	Ref	Expression
1		unexg	$$⊢\left(A\in 𝒫X\wedge B\in 𝒫X\right)\to A\cup B\in \mathrm{V}$$
2		elpwi	$$⊢A\in 𝒫X\to A\subseteq X$$
3		elpwi	$$⊢B\in 𝒫X\to B\subseteq X$$
4		unss	$$⊢\left(A\subseteq X\wedge B\subseteq X\right)\leftrightarrow A\cup B\subseteq X$$
5	4	biimpi	$$⊢\left(A\subseteq X\wedge B\subseteq X\right)\to A\cup B\subseteq X$$
6	2 3 5	syl2an	$$⊢\left(A\in 𝒫X\wedge B\in 𝒫X\right)\to A\cup B\subseteq X$$
7	1 6	elpwd	$$⊢\left(A\in 𝒫X\wedge B\in 𝒫X\right)\to A\cup B\in 𝒫X$$