Theorem elpwdifcl

Description: Closure of class difference with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020)

	Ref	Expression
Hypothesis	elpwincl.1	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 𝐶 )
Assertion	elpwdifcl	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ∈ 𝒫 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		elpwincl.1	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 𝐶 )
2	1	elpwid	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
3	2	ssdifssd	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ⊆ 𝐶 )
4		difexg	⊢ ( 𝐴 ∈ 𝒫 𝐶 → ( 𝐴 ∖ 𝐵 ) ∈ V )
5		elpwg	⊢ ( ( 𝐴 ∖ 𝐵 ) ∈ V → ( ( 𝐴 ∖ 𝐵 ) ∈ 𝒫 𝐶 ↔ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐶 ) )
6	1 4 5	3syl	⊢ ( 𝜑 → ( ( 𝐴 ∖ 𝐵 ) ∈ 𝒫 𝐶 ↔ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐶 ) )
7	3 6	mpbird	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ∈ 𝒫 𝐶 )