Theorem invdif 4232

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 4224	. 2 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ (V ∖ (V ∖ 𝐵)))
2		ddif 4095	. . 3 ⊢ (V ∖ (V ∖ 𝐵)) = 𝐵
3	2	difeq2i 4078	. 2 ⊢ (𝐴 ∖ (V ∖ (V ∖ 𝐵))) = (𝐴 ∖ 𝐵)
4	1, 3	eqtri 2788	1 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)

This proof depends on syntax axioms:   = wceq 1570  Vcvv 3457   ∖ cdif 3903   ∩ cin 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-in 3913

This theorem is used by:  indif2  4234  difundi  4243  difundir  4244  difindi  4245  difindir  4246  difdif2  4249  difun1  4252  undif1  4437  difdifdir  4454  fsuppeq  8173  fsuppeqg  8174  dfsup2  9407  fsets  17246  setsdm  17247  dmxrncnvep  39071  dmcnvepres  39072  dmxrnuncnvepres  39074