Theorem invdif 4224

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 4216	. 2 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ (V ∖ (V ∖ 𝐵)))
2		ddif 4077	. . 3 ⊢ (V ∖ (V ∖ 𝐵)) = 𝐵
3	2	difeq2i 4060	. 2 ⊢ (𝐴 ∖ (V ∖ (V ∖ 𝐵))) = (𝐴 ∖ 𝐵)
4	1, 3	eqtri 2783	1 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)

This proof depends on syntax axioms:   = wceq 1569  Vcvv 3450   ∖ cdif 4045   ∩ cin 4089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 4047  df-in 4091

This theorem is used by:  indif2  4226  difundi  4235  difundir  4236  difindi  4237  difindir  4238  difdif2  4241  difun1  4244  undif1  4429  difdifdir  4446  fsuppeq  8196  fsuppeqg  8197  dfsup2  9440  fsets  17353  setsdm  17354  dmxrncnvep  39415  dmcnvepres  39416  dmxrnuncnvepres  39418