Theorem invdif 4231

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

Assertion

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

Proof of Theorem invdif

Step	Hyp	Ref	Expression
1		dfin2 4223	. 2 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ (V ∖ (V ∖ 𝐵)))
2		ddif 4093	. . 3 ⊢ (V ∖ (V ∖ 𝐵)) = 𝐵
3	2	difeq2i 4075	. 2 ⊢ (𝐴 ∖ (V ∖ (V ∖ 𝐵))) = (𝐴 ∖ 𝐵)
4	1, 3	eqtri 2759	1 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1541  Vcvv 3440   ∖ cdif 3898   ∩ cin 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-in 3908

This theorem is referenced by:  indif2  4233  difundi  4242  difundir  4243  difindi  4244  difindir  4245  difdif2  4248  difun1  4251  undif1  4428  difdifdir  4444  fsuppeq  8117  fsuppeqg  8118  dfsup2  9347  fsets  17096  setsdm  17097  dmxrncnvep  38574  dmcnvepres  38575  dmxrnuncnvepres  38577