Theorem indif2 4222

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 4169	. 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (V ∖ 𝐶)) = (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4220	. 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶)
3		invdif 4220	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
4	3	ineq2i 4158	. 2 ⊢ (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∩ (𝐵 ∖ 𝐶))
5	1, 2, 4	3eqtr3ri 2769	1 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶)

Syntax hints:   = wceq 1542  Vcvv 3430   ∖ cdif 3887   ∩ cin 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-in 3897

This theorem is referenced by:  indif1  4223  indifcom  4224  rabdif  4262  frpoind  6302  marypha1lem  9341  frind  9669  difopn  23013  restcld  23151  difmbl  25524  voliunlem1  25531  difuncomp  32642  imadifxp  32690  psrbasfsupp  33691  difelcarsg  34474  carsgclctunlem1  34481  topbnd  36526  bj-disj2r  37355  nlpineqsn  37742  mblfinlem3  37998  mblfinlem4  37999  dmxrncnvepres2  38772  gneispace  44583  saldifcl2  46778  caragenuncllem  46962  carageniuncllem1  46971  iscnrm3rlem1  49431