Theorem difelpw

Description: A difference is an element of the power set of its minuend. (Contributed by AV, 9-Oct-2023)

	Ref	Expression
Assertion	difelpw	$$⊢A\in V\to A\setminus B\in 𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		difss	$$⊢A\setminus B\subseteq A$$
2		elpw2g	$$⊢A\in V\to \left(A\setminus B\in 𝒫A\leftrightarrow A\setminus B\subseteq A\right)$$
3	1 2	mpbiri	$$⊢A\in V\to A\setminus B\in 𝒫A$$