Metamath Proof Explorer

Theorem wrddin2

Description: Distribution of word class constructor over class intersection. (Contributed by Ender Ting, 24-Jul-2026)

Ref Expression
Assertion wrddin2 ⊢ Word B ∩ C = Word B ∩ Word C

Proof

Step Hyp Ref Expression
1 wrddrin ⊢ n ∈ Word B ∩ C → n ∈ Word B ∧ n ∈ Word C
2 wrddin ⊢ n ∈ Word B ∧ n ∈ Word C → n ∈ Word B ∩ C
3 1 2 impbii ⊢ n ∈ Word B ∩ C ↔ n ∈ Word B ∧ n ∈ Word C
4 elin ⊢ n ∈ Word B ∩ Word C ↔ n ∈ Word B ∧ n ∈ Word C
5 3 4 bitr4i ⊢ n ∈ Word B ∩ C ↔ n ∈ Word B ∩ Word C
6 5 eqriv ⊢ Word B ∩ C = Word B ∩ Word C