Theorem invdif

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

	Ref	Expression
Assertion	invdif	⊢ ( 𝐴 ∩ ( V ∖ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dfin2	⊢ ( 𝐴 ∩ ( V ∖ 𝐵 ) ) = ( 𝐴 ∖ ( V ∖ ( V ∖ 𝐵 ) ) )
2		ddif	⊢ ( V ∖ ( V ∖ 𝐵 ) ) = 𝐵
3	2	difeq2i	⊢ ( 𝐴 ∖ ( V ∖ ( V ∖ 𝐵 ) ) ) = ( 𝐴 ∖ 𝐵 )
4	1 3	eqtri	⊢ ( 𝐴 ∩ ( V ∖ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 )