This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )