Theorem wrddrin

Description: A word whose alphabet is intersection of two classes is also a word in each of those alphabets. (Contributed by Ender Ting, 24-Jul-2026)

	Ref	Expression
Assertion	wrddrin	|- ( A e. Word ( B i^i C ) -> ( A e. Word B /\ A e. Word C ) )

Proof

Step	Hyp	Ref	Expression
1		inss1	|- ( B i^i C ) C_ B
2		sswrd	|- ( ( B i^i C ) C_ B -> Word ( B i^i C ) C_ Word B )
3	1 2	ax-mp	|- Word ( B i^i C ) C_ Word B
4	3	sseli	|- ( A e. Word ( B i^i C ) -> A e. Word B )
5		inss2	|- ( B i^i C ) C_ C
6		sswrd	|- ( ( B i^i C ) C_ C -> Word ( B i^i C ) C_ Word C )
7	5 6	ax-mp	|- Word ( B i^i C ) C_ Word C
8	7	sseli	|- ( A e. Word ( B i^i C ) -> A e. Word C )
9	4 8	jca	|- ( A e. Word ( B i^i C ) -> ( A e. Word B /\ A e. Word C ) )