Theorem indif2 4226

Description: Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.)

Assertion

Ref	Expression
indif2	⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶)

Proof of Theorem indif2

Step	Hyp	Ref	Expression
1		inass 4124	. 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (V ∖ 𝐶)) = (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4224	. 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶)
3		invdif 4224	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
4	3	ineq2i 4114	. 2 ⊢ (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∩ (𝐵 ∖ 𝐶))
5	1, 2, 4	3eqtr3ri 2792	1 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶)

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:  indif1  4227  indifcom  4228  rabdif  4266  inssdif0  4321  frpoind  6345  marypha1lem  9425  frind  9754  difopn  23352  restcld  23490  difmbl  25864  voliunlem1  25871  difuncomp  33148  imadifxp  33195  psrbasfsupp  34143  difelcarsg  34942  carsgclctunlem1  34949  topbnd  37112  bj-disj2r  37941  nlpineqsn  38332  mblfinlem3  38578  mblfinlem4  38579  dmxrncnvepres2  39366  gneispace  45134  saldifcl2  47338  caragenuncllem  47522  carageniuncllem1  47531  iscnrm3rlem1  50048