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