Metamath Proof Explorer


Theorem indifdi

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

Ref Expression
Assertion indifdi ABC=ABAC

Proof

Step Hyp Ref Expression
1 elin xABCxAxBC
2 eldif xBCxB¬xC
3 2 anbi2i xAxBCxAxB¬xC
4 abai xA¬xCxAxA¬xC
5 4 anbi2i xBxA¬xCxBxAxA¬xC
6 an12 xAxB¬xCxBxA¬xC
7 eldif xABACxAB¬xAC
8 elin xABxAxB
9 8 bicomi xAxBxAB
10 imnan xA¬xC¬xAxC
11 elin xACxAxC
12 10 11 xchbinxr xA¬xC¬xAC
13 9 12 anbi12i xAxBxA¬xCxAB¬xAC
14 an21 xAxBxA¬xCxBxAxA¬xC
15 7 13 14 3bitr2i xABACxBxAxA¬xC
16 5 6 15 3bitr4i xAxB¬xCxABAC
17 1 3 16 3bitri xABCxABAC
18 17 eqriv ABC=ABAC