Metamath Proof Explorer


Theorem pwpwuni

Description: Relationship between power class and union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion pwpwuni A V A 𝒫 𝒫 B A 𝒫 B

Proof

Step Hyp Ref Expression
1 elpwg A V A 𝒫 𝒫 B A 𝒫 B
2 sspwuni A 𝒫 B A B
3 2 a1i A V A 𝒫 B A B
4 uniexg A V A V
5 elpwg A V A 𝒫 B A B
6 4 5 syl A V A 𝒫 B A B
7 6 bicomd A V A B A 𝒫 B
8 1 3 7 3bitrd A V A 𝒫 𝒫 B A 𝒫 B