Theorem wrddin2

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

	Ref	Expression
Assertion	wrddin2	|- Word ( B i^i C ) = ( Word B i^i Word C )

Proof

Step	Hyp	Ref	Expression
1		wrddrin	|- ( n e. Word ( B i^i C ) -> ( n e. Word B /\ n e. Word C ) )
2		wrddin	|- ( ( n e. Word B /\ n e. Word C ) -> n e. Word ( B i^i C ) )
3	1 2	impbii	|- ( n e. Word ( B i^i C ) <-> ( n e. Word B /\ n e. Word C ) )
4		elin	|- ( n e. ( Word B i^i Word C ) <-> ( n e. Word B /\ n e. Word C ) )
5	3 4	bitr4i	|- ( n e. Word ( B i^i C ) <-> n e. ( Word B i^i Word C ) )
6	5	eqriv	|- Word ( B i^i C ) = ( Word B i^i Word C )