Theorem indif2 4240

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 4186	. 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (V ∖ 𝐶)) = (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4238	. 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶)
3		invdif 4238	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
4	3	ineq2i 4176	. 2 ⊢ (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∩ (𝐵 ∖ 𝐶))
5	1, 2, 4	3eqtr3ri 2801	1 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶)

Syntax hints:   = wceq 1567  Vcvv 3461   ∖ cdif 3908   ∩ cin 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-dif 3914  df-in 3918

This theorem is referenced by:  indif1  4241  indifcom  4242  rabdif  4280  frpoind  6344  marypha1lem  9393  frind  9722  difopn  23160  restcld  23298  difmbl  25671  voliunlem1  25678  difuncomp  32839  imadifxp  32887  psrbasfsupp  33846  difelcarsg  34645  carsgclctunlem1  34652  topbnd  36758  bj-disj2r  37587  nlpineqsn  37977  mblfinlem3  38233  mblfinlem4  38234  dmxrncnvepres2  39007  gneispace  44787  saldifcl2  46969  caragenuncllem  47153  carageniuncllem1  47162  iscnrm3rlem1  49638