Theorem indif1 4205

Description: Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015.)

Assertion

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

Proof of Theorem indif1

Step	Hyp	Ref	Expression
1		indif2 4204	. 2 ⊢ (𝐵 ∩ (𝐴 ∖ 𝐶)) = ((𝐵 ∩ 𝐴) ∖ 𝐶)
2		incom 4135	. 2 ⊢ (𝐵 ∩ (𝐴 ∖ 𝐶)) = ((𝐴 ∖ 𝐶) ∩ 𝐵)
3		incom 4135	. . 3 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
4	3	difeq1i 4053	. 2 ⊢ ((𝐵 ∩ 𝐴) ∖ 𝐶) = ((𝐴 ∩ 𝐵) ∖ 𝐶)
5	1, 2, 4	3eqtr3i 2774	1 ⊢ ((𝐴 ∖ 𝐶) ∩ 𝐵) = ((𝐴 ∩ 𝐵) ∖ 𝐶)

Syntax hints:   = wceq 1539   ∖ cdif 3884   ∩ cin 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-in 3894

This theorem is referenced by:  resdifcom  5910  resdmdfsn  5941  hartogslem1  9301  fpwwe2  10399  leiso  14173  basdif0  22103  tgdif0  22142  kqdisj  22883  trufil  23061  difininv  30864  gtiso  31033  dfon4  34195  disjdifb  46155