Metamath Proof Explorer

Theorem eldifpw

Description: Membership in a power class difference. (Contributed by NM, 25-Mar-2007)

Ref Expression
Hypothesis eldifpw.1 ⊢ C ∈ V
Assertion eldifpw ⊢ A ∈ 𝒫 B ∧ ¬ C ⊆ B → A ∪ C ∈ 𝒫 B ∪ C ∖ 𝒫 B

Proof

Step Hyp Ref Expression
1 eldifpw.1 ⊢ C ∈ V
2 elpwi ⊢ A ∈ 𝒫 B → A ⊆ B
3 unss1 ⊢ A ⊆ B → A ∪ C ⊆ B ∪ C
4 unexg ⊢ A ∈ 𝒫 B ∧ C ∈ V → A ∪ C ∈ V
5 1 4 mpan2 ⊢ A ∈ 𝒫 B → A ∪ C ∈ V
6 elpwg ⊢ A ∪ C ∈ V → A ∪ C ∈ 𝒫 B ∪ C ↔ A ∪ C ⊆ B ∪ C
7 5 6 syl ⊢ A ∈ 𝒫 B → A ∪ C ∈ 𝒫 B ∪ C ↔ A ∪ C ⊆ B ∪ C
8 3 7 imbitrrid ⊢ A ∈ 𝒫 B → A ⊆ B → A ∪ C ∈ 𝒫 B ∪ C
9 2 8 mpd ⊢ A ∈ 𝒫 B → A ∪ C ∈ 𝒫 B ∪ C
10 elpwi ⊢ A ∪ C ∈ 𝒫 B → A ∪ C ⊆ B
11 10 unssbd ⊢ A ∪ C ∈ 𝒫 B → C ⊆ B
12 11 con3i ⊢ ¬ C ⊆ B → ¬ A ∪ C ∈ 𝒫 B
13 9 12 anim12i ⊢ A ∈ 𝒫 B ∧ ¬ C ⊆ B → A ∪ C ∈ 𝒫 B ∪ C ∧ ¬ A ∪ C ∈ 𝒫 B
14 eldif ⊢ A ∪ C ∈ 𝒫 B ∪ C ∖ 𝒫 B ↔ A ∪ C ∈ 𝒫 B ∪ C ∧ ¬ A ∪ C ∈ 𝒫 B
15 13 14 sylibr ⊢ A ∈ 𝒫 B ∧ ¬ C ⊆ B → A ∪ C ∈ 𝒫 B ∪ C ∖ 𝒫 B