# Metamath Proof Explorer

## Theorem eldifpw

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

Ref Expression
Hypothesis eldifpw.1 𝐶 ∈ V
Assertion eldifpw ( ( 𝐴 ∈ 𝒫 𝐵 ∧ ¬ 𝐶𝐵 ) → ( 𝐴𝐶 ) ∈ ( 𝒫 ( 𝐵𝐶 ) ∖ 𝒫 𝐵 ) )

### Proof

Step Hyp Ref Expression
1 eldifpw.1 𝐶 ∈ V
2 elpwi ( 𝐴 ∈ 𝒫 𝐵𝐴𝐵 )
3 unss1 ( 𝐴𝐵 → ( 𝐴𝐶 ) ⊆ ( 𝐵𝐶 ) )
4 unexg ( ( 𝐴 ∈ 𝒫 𝐵𝐶 ∈ V ) → ( 𝐴𝐶 ) ∈ V )
5 1 4 mpan2 ( 𝐴 ∈ 𝒫 𝐵 → ( 𝐴𝐶 ) ∈ V )
6 elpwg ( ( 𝐴𝐶 ) ∈ V → ( ( 𝐴𝐶 ) ∈ 𝒫 ( 𝐵𝐶 ) ↔ ( 𝐴𝐶 ) ⊆ ( 𝐵𝐶 ) ) )
7 5 6 syl ( 𝐴 ∈ 𝒫 𝐵 → ( ( 𝐴𝐶 ) ∈ 𝒫 ( 𝐵𝐶 ) ↔ ( 𝐴𝐶 ) ⊆ ( 𝐵𝐶 ) ) )
8 3 7 syl5ibr ( 𝐴 ∈ 𝒫 𝐵 → ( 𝐴𝐵 → ( 𝐴𝐶 ) ∈ 𝒫 ( 𝐵𝐶 ) ) )
9 2 8 mpd ( 𝐴 ∈ 𝒫 𝐵 → ( 𝐴𝐶 ) ∈ 𝒫 ( 𝐵𝐶 ) )
10 elpwi ( ( 𝐴𝐶 ) ∈ 𝒫 𝐵 → ( 𝐴𝐶 ) ⊆ 𝐵 )
11 10 unssbd ( ( 𝐴𝐶 ) ∈ 𝒫 𝐵𝐶𝐵 )
12 11 con3i ( ¬ 𝐶𝐵 → ¬ ( 𝐴𝐶 ) ∈ 𝒫 𝐵 )
13 9 12 anim12i ( ( 𝐴 ∈ 𝒫 𝐵 ∧ ¬ 𝐶𝐵 ) → ( ( 𝐴𝐶 ) ∈ 𝒫 ( 𝐵𝐶 ) ∧ ¬ ( 𝐴𝐶 ) ∈ 𝒫 𝐵 ) )
14 eldif ( ( 𝐴𝐶 ) ∈ ( 𝒫 ( 𝐵𝐶 ) ∖ 𝒫 𝐵 ) ↔ ( ( 𝐴𝐶 ) ∈ 𝒫 ( 𝐵𝐶 ) ∧ ¬ ( 𝐴𝐶 ) ∈ 𝒫 𝐵 ) )
15 13 14 sylibr ( ( 𝐴 ∈ 𝒫 𝐵 ∧ ¬ 𝐶𝐵 ) → ( 𝐴𝐶 ) ∈ ( 𝒫 ( 𝐵𝐶 ) ∖ 𝒫 𝐵 ) )