# Metamath Proof Explorer

## Theorem eldifpw

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

Ref Expression
Hypothesis eldifpw.1 ${⊢}{C}\in \mathrm{V}$
Assertion eldifpw ${⊢}\left({A}\in 𝒫{B}\wedge ¬{C}\subseteq {B}\right)\to {A}\cup {C}\in \left(𝒫\left({B}\cup {C}\right)\setminus 𝒫{B}\right)$

### Proof

Step Hyp Ref Expression
1 eldifpw.1 ${⊢}{C}\in \mathrm{V}$
2 elpwi ${⊢}{A}\in 𝒫{B}\to {A}\subseteq {B}$
3 unss1 ${⊢}{A}\subseteq {B}\to {A}\cup {C}\subseteq {B}\cup {C}$
4 unexg ${⊢}\left({A}\in 𝒫{B}\wedge {C}\in \mathrm{V}\right)\to {A}\cup {C}\in \mathrm{V}$
5 1 4 mpan2 ${⊢}{A}\in 𝒫{B}\to {A}\cup {C}\in \mathrm{V}$
6 elpwg ${⊢}{A}\cup {C}\in \mathrm{V}\to \left({A}\cup {C}\in 𝒫\left({B}\cup {C}\right)↔{A}\cup {C}\subseteq {B}\cup {C}\right)$
7 5 6 syl ${⊢}{A}\in 𝒫{B}\to \left({A}\cup {C}\in 𝒫\left({B}\cup {C}\right)↔{A}\cup {C}\subseteq {B}\cup {C}\right)$
8 3 7 syl5ibr ${⊢}{A}\in 𝒫{B}\to \left({A}\subseteq {B}\to {A}\cup {C}\in 𝒫\left({B}\cup {C}\right)\right)$
9 2 8 mpd ${⊢}{A}\in 𝒫{B}\to {A}\cup {C}\in 𝒫\left({B}\cup {C}\right)$
10 elpwi ${⊢}{A}\cup {C}\in 𝒫{B}\to {A}\cup {C}\subseteq {B}$
11 10 unssbd ${⊢}{A}\cup {C}\in 𝒫{B}\to {C}\subseteq {B}$
12 11 con3i ${⊢}¬{C}\subseteq {B}\to ¬{A}\cup {C}\in 𝒫{B}$
13 9 12 anim12i ${⊢}\left({A}\in 𝒫{B}\wedge ¬{C}\subseteq {B}\right)\to \left({A}\cup {C}\in 𝒫\left({B}\cup {C}\right)\wedge ¬{A}\cup {C}\in 𝒫{B}\right)$
14 eldif ${⊢}{A}\cup {C}\in \left(𝒫\left({B}\cup {C}\right)\setminus 𝒫{B}\right)↔\left({A}\cup {C}\in 𝒫\left({B}\cup {C}\right)\wedge ¬{A}\cup {C}\in 𝒫{B}\right)$
15 13 14 sylibr ${⊢}\left({A}\in 𝒫{B}\wedge ¬{C}\subseteq {B}\right)\to {A}\cup {C}\in \left(𝒫\left({B}\cup {C}\right)\setminus 𝒫{B}\right)$