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	$$⊢\phi \to A\in 𝒫C$$
Assertion	elpwdifcl	$$⊢\phi \to A\setminus B\in 𝒫C$$

Proof

Step	Hyp	Ref	Expression
1		elpwincl.1	$$⊢\phi \to A\in 𝒫C$$
2	1	elpwid	$$⊢\phi \to A\subseteq C$$
3	2	ssdifssd	$$⊢\phi \to A\setminus B\subseteq C$$
4		difexg	$$⊢A\in 𝒫C\to A\setminus B\in \mathrm{V}$$
5		elpwg	$$⊢A\setminus B\in \mathrm{V}\to \left(A\setminus B\in 𝒫C\leftrightarrow A\setminus B\subseteq C\right)$$
6	1 4 5	3syl	$$⊢\phi \to \left(A\setminus B\in 𝒫C\leftrightarrow A\setminus B\subseteq C\right)$$
7	3 6	mpbird	$$⊢\phi \to A\setminus B\in 𝒫C$$