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	imbitrrid	⊢ ( 𝐴 ∈ 𝒫 𝐵 → ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 ( 𝐵 ∪ 𝐶 ) ) )
9	2 8	mpd	⊢ ( 𝐴 ∈ 𝒫 𝐵 → ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 ( 𝐵 ∪ 𝐶 ) )
10		elpwi	⊢ ( ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 𝐵 → ( 𝐴 ∪ 𝐶 ) ⊆ 𝐵 )
11	10	unssbd	⊢ ( ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 𝐵 → 𝐶 ⊆ 𝐵 )
12	11	con3i	⊢ ( ¬ 𝐶 ⊆ 𝐵 → ¬ ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 𝐵 )
13	9 12	anim12i	⊢ ( ( 𝐴 ∈ 𝒫 𝐵 ∧ ¬ 𝐶 ⊆ 𝐵 ) → ( ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 ( 𝐵 ∪ 𝐶 ) ∧ ¬ ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 𝐵 ) )
14		eldif	⊢ ( ( 𝐴 ∪ 𝐶 ) ∈ ( 𝒫 ( 𝐵 ∪ 𝐶 ) ∖ 𝒫 𝐵 ) ↔ ( ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 ( 𝐵 ∪ 𝐶 ) ∧ ¬ ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 𝐵 ) )
15	13 14	sylibr	⊢ ( ( 𝐴 ∈ 𝒫 𝐵 ∧ ¬ 𝐶 ⊆ 𝐵 ) → ( 𝐴 ∪ 𝐶 ) ∈ ( 𝒫 ( 𝐵 ∪ 𝐶 ) ∖ 𝒫 𝐵 ) )