Theorem indif2 4212

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 4159	. 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (V ∖ 𝐶)) = (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4210	. 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶)
3		invdif 4210	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
4	3	ineq2i 4149	. 2 ⊢ (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∩ (𝐵 ∖ 𝐶))
5	1, 2, 4	3eqtr3ri 2773	1 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶)

Syntax hints:   = wceq 1548  Vcvv 3433   ∖ cdif 3882   ∩ cin 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-in 3892

This theorem is referenced by:  indif1  4213  indifcom  4214  rabdif  4252  frpoind  6297  marypha1lem  9340  frind  9669  difopn  23021  restcld  23159  difmbl  25532  voliunlem1  25539  difuncomp  32646  imadifxp  32694  psrbasfsupp  33707  difelcarsg  34506  carsgclctunlem1  34513  topbnd  36567  bj-disj2r  37396  nlpineqsn  37785  mblfinlem3  38041  mblfinlem4  38042  dmxrncnvepres2  38815  gneispace  44593  saldifcl2  46785  caragenuncllem  46969  carageniuncllem1  46978  iscnrm3rlem1  49444