Theorem invdif

Description: Intersection with universal complement. Remark in Stoll p. 20. (Contributed by NM, 17-Aug-2004)

	Ref	Expression
Assertion	invdif	$$⊢A\cap \left(\mathrm{V}\setminus B\right)=A\setminus B$$

Proof

Step	Hyp	Ref	Expression
1		dfin2	$$⊢A\cap \left(\mathrm{V}\setminus B\right)=A\setminus \left(\mathrm{V}\setminus \left(\mathrm{V}\setminus B\right)\right)$$
2		ddif	$$⊢\mathrm{V}\setminus \left(\mathrm{V}\setminus B\right)=B$$
3	2	difeq2i	$$⊢A\setminus \left(\mathrm{V}\setminus \left(\mathrm{V}\setminus B\right)\right)=A\setminus B$$
4	1 3	eqtri	$$⊢A\cap \left(\mathrm{V}\setminus B\right)=A\setminus B$$