Metamath Proof Explorer

Theorem elpwun

Description: Membership in the power class of a union. (Contributed by NM, 26-Mar-2007)

Ref Expression
Hypothesis eldifpw.1 ⊢ C ∈ V
Assertion elpwun ⊢ A ∈ 𝒫 B ∪ C ↔ A ∖ C ∈ 𝒫 B

Proof

Step Hyp Ref Expression
1 eldifpw.1 ⊢ C ∈ V
2 elex ⊢ A ∈ 𝒫 B ∪ C → A ∈ V
3 elex ⊢ A ∖ C ∈ 𝒫 B → A ∖ C ∈ V
4 difex2 ⊢ C ∈ V → A ∈ V ↔ A ∖ C ∈ V
5 1 4 ax-mp ⊢ A ∈ V ↔ A ∖ C ∈ V
6 3 5 sylibr ⊢ A ∖ C ∈ 𝒫 B → A ∈ V
7 elpwg ⊢ A ∈ V → A ∈ 𝒫 B ∪ C ↔ A ⊆ B ∪ C
8 uncom ⊢ B ∪ C = C ∪ B
9 8 sseq2i ⊢ A ⊆ B ∪ C ↔ A ⊆ C ∪ B
10 ssundif ⊢ A ⊆ C ∪ B ↔ A ∖ C ⊆ B
11 9 10 bitri ⊢ A ⊆ B ∪ C ↔ A ∖ C ⊆ B
12 difexg ⊢ A ∈ V → A ∖ C ∈ V
13 elpwg ⊢ A ∖ C ∈ V → A ∖ C ∈ 𝒫 B ↔ A ∖ C ⊆ B
14 12 13 syl ⊢ A ∈ V → A ∖ C ∈ 𝒫 B ↔ A ∖ C ⊆ B
15 11 14 bitr4id ⊢ A ∈ V → A ⊆ B ∪ C ↔ A ∖ C ∈ 𝒫 B
16 7 15 bitrd ⊢ A ∈ V → A ∈ 𝒫 B ∪ C ↔ A ∖ C ∈ 𝒫 B
17 2 6 16 pm5.21nii ⊢ A ∈ 𝒫 B ∪ C ↔ A ∖ C ∈ 𝒫 B