Theorem indif2 4227

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 4173	. 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (V ∖ 𝐶)) = (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4225	. 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶)
3		invdif 4225	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
4	3	ineq2i 4163	. 2 ⊢ (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∩ (𝐵 ∖ 𝐶))
5	1, 2, 4	3eqtr3ri 2793	1 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶)

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 3900  df-in 3904

This theorem is used by:  indif1  4228  indifcom  4229  rabdif  4267  inssdif0  4322  frpoind  6346  marypha1lem  9426  frind  9755  difopn  23353  restcld  23491  difmbl  25865  voliunlem1  25872  difuncomp  33149  imadifxp  33196  psrbasfsupp  34144  difelcarsg  34943  carsgclctunlem1  34950  topbnd  37113  bj-disj2r  37942  nlpineqsn  38333  mblfinlem3  38579  mblfinlem4  38580  dmxrncnvepres2  39367  gneispace  45135  saldifcl2  47339  caragenuncllem  47523  carageniuncllem1  47532  iscnrm3rlem1  50049