Theorem pwuncl

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

	Ref	Expression
Assertion	pwuncl	|- ( ( A e. ~P X /\ B e. ~P X ) -> ( A u. B ) e. ~P X )

Proof

Step	Hyp	Ref	Expression
1		unexg	|- ( ( A e. ~P X /\ B e. ~P X ) -> ( A u. B ) e. _V )
2		elpwi	|- ( A e. ~P X -> A C_ X )
3		elpwi	|- ( B e. ~P X -> B C_ X )
4		unss	|- ( ( A C_ X /\ B C_ X ) <-> ( A u. B ) C_ X )
5	4	biimpi	|- ( ( A C_ X /\ B C_ X ) -> ( A u. B ) C_ X )
6	2 3 5	syl2an	|- ( ( A e. ~P X /\ B e. ~P X ) -> ( A u. B ) C_ X )
7	1 6	elpwd	|- ( ( A e. ~P X /\ B e. ~P X ) -> ( A u. B ) e. ~P X )