Theorem invdif 4228

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 4220	. 2 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ (V ∖ (V ∖ 𝐵)))
2		ddif 4090	. . 3 ⊢ (V ∖ (V ∖ 𝐵)) = 𝐵
3	2	difeq2i 4072	. 2 ⊢ (𝐴 ∖ (V ∖ (V ∖ 𝐵))) = (𝐴 ∖ 𝐵)
4	1, 3	eqtri 2756	1 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)

Syntax hints:   = wceq 1541  Vcvv 3437   ∖ cdif 3895   ∩ cin 3897

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-in 3905

This theorem is referenced by:  indif2  4230  difundi  4239  difundir  4240  difindi  4241  difindir  4242  difdif2  4245  difun1  4248  undif1  4425  difdifdir  4441  fsuppeq  8114  fsuppeqg  8115  dfsup2  9339  fsets  17087  setsdm  17088  dmxrncnvep  38486  dmcnvepres  38487  dmxrnuncnvepres  38489