This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pwundif

Description: Break up the power class of a union into a union of smaller classes. (Contributed by NM, 25-Mar-2007) (Proof shortened by Thierry Arnoux, 20-Dec-2016) Remove use of ax-sep , ax-nul , ax-pr and shorten proof. (Revised by BJ, 14-Apr-2024)

Ref Expression
Assertion pwundif ⊢ 𝒫 A ∪ B = 𝒫 A ∪ B ∖ 𝒫 A ∪ 𝒫 A

Proof

Step Hyp Ref Expression
1 ssun1 ⊢ A ⊆ A ∪ B
2 1 sspwi ⊢ 𝒫 A ⊆ 𝒫 A ∪ B
3 undif ⊢ 𝒫 A ⊆ 𝒫 A ∪ B ↔ 𝒫 A ∪ 𝒫 A ∪ B ∖ 𝒫 A = 𝒫 A ∪ B
4 2 3 mpbi ⊢ 𝒫 A ∪ 𝒫 A ∪ B ∖ 𝒫 A = 𝒫 A ∪ B
5 uncom ⊢ 𝒫 A ∪ 𝒫 A ∪ B ∖ 𝒫 A = 𝒫 A ∪ B ∖ 𝒫 A ∪ 𝒫 A
6 4 5 eqtr3i ⊢ 𝒫 A ∪ B = 𝒫 A ∪ B ∖ 𝒫 A ∪ 𝒫 A