Theorem invdif 4225

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 4217	. 2 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ (V ∖ (V ∖ 𝐵)))
2		ddif 4088	. . 3 ⊢ (V ∖ (V ∖ 𝐵)) = 𝐵
3	2	difeq2i 4071	. 2 ⊢ (𝐴 ∖ (V ∖ (V ∖ 𝐵))) = (𝐴 ∖ 𝐵)
4	1, 3	eqtri 2784	1 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)

This proof depends on syntax axioms:   = wceq 1570  Vcvv 3451   ∖ cdif 3896   ∩ cin 3898

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-in 3906

This theorem is used by:  indif2  4227  difundi  4236  difundir  4237  difindi  4238  difindir  4239  difdif2  4242  difun1  4245  undif1  4430  difdifdir  4447  fsuppeq  8185  fsuppeqg  8186  dfsup2  9429  fsets  17340  setsdm  17341  dmxrncnvep  39301  dmcnvepres  39302  dmxrnuncnvepres  39304