Metamath Proof Explorer

Theorem indifdirOLD

Description: Obsolete version of indifdir as of 14-Aug-2024. (Contributed by Scott Fenton, 14-Apr-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion indifdirOLD ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) = ( ( 𝐴 ∩ 𝐶 ) ∖ ( 𝐵 ∩ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 pm3.24 ⊢ ¬ ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐶 )
2 1 intnan ⊢ ¬ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐶 ) )
3 anass ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ¬ 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
4 2 3 mtbir ⊢ ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ¬ 𝑥 ∈ 𝐶 )
5 4 biorfi ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ¬ 𝑥 ∈ 𝐵 ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ¬ 𝑥 ∈ 𝐵 ) ∨ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
6 an32 ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ¬ 𝑥 ∈ 𝐵 ) )
7 andi ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥 ∈ 𝐶 ) ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ¬ 𝑥 ∈ 𝐵 ) ∨ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
8 5 6 7 3bitr4i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥 ∈ 𝐶 ) ) )
9 ianor ⊢ ( ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ↔ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥 ∈ 𝐶 ) )
10 9 anbi2i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥 ∈ 𝐶 ) ) )
11 8 10 bitr4i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) )
12 elin ⊢ ( 𝑥 ∈ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ↔ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) )
13 eldif ⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) )
14 13 anbi1i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) )
15 12 14 bitri ⊢ ( 𝑥 ∈ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) )
16 eldif ⊢ ( 𝑥 ∈ ( ( 𝐴 ∩ 𝐶 ) ∖ ( 𝐵 ∩ 𝐶 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ ¬ 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ) )
17 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) )
18 elin ⊢ ( 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) )
19 18 notbii ⊢ ( ¬ 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) )
20 17 19 anbi12i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ ¬ 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) )
21 16 20 bitri ⊢ ( 𝑥 ∈ ( ( 𝐴 ∩ 𝐶 ) ∖ ( 𝐵 ∩ 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ∧ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) )
22 11 15 21 3bitr4i ⊢ ( 𝑥 ∈ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ↔ 𝑥 ∈ ( ( 𝐴 ∩ 𝐶 ) ∖ ( 𝐵 ∩ 𝐶 ) ) )
23 22 eqriv ⊢ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) = ( ( 𝐴 ∩ 𝐶 ) ∖ ( 𝐵 ∩ 𝐶 ) )