Theorem indifdi

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

	Ref	Expression
Assertion	indifdi	|- ( A i^i ( B \ C ) ) = ( ( A i^i B ) \ ( A i^i C ) )

Proof

Step	Hyp	Ref	Expression
1		elin	|- ( x e. ( A i^i ( B \ C ) ) <-> ( x e. A /\ x e. ( B \ C ) ) )
2		eldif	|- ( x e. ( B \ C ) <-> ( x e. B /\ -. x e. C ) )
3	2	anbi2i	|- ( ( x e. A /\ x e. ( B \ C ) ) <-> ( x e. A /\ ( x e. B /\ -. x e. C ) ) )
4		abai	|- ( ( x e. A /\ -. x e. C ) <-> ( x e. A /\ ( x e. A -> -. x e. C ) ) )
5	4	anbi2i	|- ( ( x e. B /\ ( x e. A /\ -. x e. C ) ) <-> ( x e. B /\ ( x e. A /\ ( x e. A -> -. x e. C ) ) ) )
6		an12	|- ( ( x e. A /\ ( x e. B /\ -. x e. C ) ) <-> ( x e. B /\ ( x e. A /\ -. x e. C ) ) )
7		eldif	|- ( x e. ( ( A i^i B ) \ ( A i^i C ) ) <-> ( x e. ( A i^i B ) /\ -. x e. ( A i^i C ) ) )
8		elin	|- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
9	8	bicomi	|- ( ( x e. A /\ x e. B ) <-> x e. ( A i^i B ) )
10		imnan	|- ( ( x e. A -> -. x e. C ) <-> -. ( x e. A /\ x e. C ) )
11		elin	|- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
12	10 11	xchbinxr	|- ( ( x e. A -> -. x e. C ) <-> -. x e. ( A i^i C ) )
13	9 12	anbi12i	|- ( ( ( x e. A /\ x e. B ) /\ ( x e. A -> -. x e. C ) ) <-> ( x e. ( A i^i B ) /\ -. x e. ( A i^i C ) ) )
14		an21	|- ( ( ( x e. A /\ x e. B ) /\ ( x e. A -> -. x e. C ) ) <-> ( x e. B /\ ( x e. A /\ ( x e. A -> -. x e. C ) ) ) )
15	7 13 14	3bitr2i	|- ( x e. ( ( A i^i B ) \ ( A i^i C ) ) <-> ( x e. B /\ ( x e. A /\ ( x e. A -> -. x e. C ) ) ) )
16	5 6 15	3bitr4i	|- ( ( x e. A /\ ( x e. B /\ -. x e. C ) ) <-> x e. ( ( A i^i B ) \ ( A i^i C ) ) )
17	1 3 16	3bitri	|- ( x e. ( A i^i ( B \ C ) ) <-> x e. ( ( A i^i B ) \ ( A i^i C ) ) )
18	17	eqriv	|- ( A i^i ( B \ C ) ) = ( ( A i^i B ) \ ( A i^i C ) )