Metamath Proof Explorer


Theorem pwuncl

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

Ref Expression
Assertion pwuncl A𝒫XB𝒫XAB𝒫X

Proof

Step Hyp Ref Expression
1 unexg A𝒫XB𝒫XABV
2 elpwi A𝒫XAX
3 elpwi B𝒫XBX
4 unss AXBXABX
5 4 biimpi AXBXABX
6 2 3 5 syl2an A𝒫XB𝒫XABX
7 1 6 elpwd A𝒫XB𝒫XAB𝒫X