Theorem wrddin2

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

	Ref	Expression
Assertion	wrddin2	⊢ Word ( 𝐵 ∩ 𝐶 ) = ( Word 𝐵 ∩ Word 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		wrddrin	⊢ ( 𝑛 ∈ Word ( 𝐵 ∩ 𝐶 ) → ( 𝑛 ∈ Word 𝐵 ∧ 𝑛 ∈ Word 𝐶 ) )
2		wrddin	⊢ ( ( 𝑛 ∈ Word 𝐵 ∧ 𝑛 ∈ Word 𝐶 ) → 𝑛 ∈ Word ( 𝐵 ∩ 𝐶 ) )
3	1 2	impbii	⊢ ( 𝑛 ∈ Word ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑛 ∈ Word 𝐵 ∧ 𝑛 ∈ Word 𝐶 ) )
4		elin	⊢ ( 𝑛 ∈ ( Word 𝐵 ∩ Word 𝐶 ) ↔ ( 𝑛 ∈ Word 𝐵 ∧ 𝑛 ∈ Word 𝐶 ) )
5	3 4	bitr4i	⊢ ( 𝑛 ∈ Word ( 𝐵 ∩ 𝐶 ) ↔ 𝑛 ∈ ( Word 𝐵 ∩ Word 𝐶 ) )
6	5	eqriv	⊢ Word ( 𝐵 ∩ 𝐶 ) = ( Word 𝐵 ∩ Word 𝐶 )