Theorem indifdi

Description: Distribute intersection over difference. (Contributed by BTernaryTau, 14-Aug-2024)

	Ref	Expression
Assertion	indifdi	⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) = ( ( 𝐴 ∩ 𝐵 ) ∖ ( 𝐴 ∩ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		elin	⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ) )
2		eldif	⊢ ( 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) )
3	2	anbi2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
4		abai	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐶 ) ) )
5	4	anbi2i	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐶 ) ) ) )
6		an12	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
7		eldif	⊢ ( 𝑥 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ ( 𝐴 ∩ 𝐶 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ¬ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) )
8		elin	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
9	8	bicomi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
10		imnan	⊢ ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐶 ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) )
11		elin	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) )
12	10 11	xchbinxr	⊢ ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐶 ) ↔ ¬ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) )
13	9 12	anbi12i	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐶 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ¬ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) )
14		an21	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐶 ) ) ) )
15	7 13 14	3bitr2i	⊢ ( 𝑥 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ ( 𝐴 ∩ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐶 ) ) ) )
16	5 6 15	3bitr4i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) ↔ 𝑥 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ ( 𝐴 ∩ 𝐶 ) ) )
17	1 3 16	3bitri	⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) ↔ 𝑥 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ ( 𝐴 ∩ 𝐶 ) ) )
18	17	eqriv	⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) = ( ( 𝐴 ∩ 𝐵 ) ∖ ( 𝐴 ∩ 𝐶 ) )