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	⊢ ( 𝐴 ∈ Word ( 𝐵 ∩ 𝐶 ) → ( 𝐴 ∈ Word 𝐵 ∧ 𝐴 ∈ Word 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		inss1	⊢ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐵
2		sswrd	⊢ ( ( 𝐵 ∩ 𝐶 ) ⊆ 𝐵 → Word ( 𝐵 ∩ 𝐶 ) ⊆ Word 𝐵 )
3	1 2	ax-mp	⊢ Word ( 𝐵 ∩ 𝐶 ) ⊆ Word 𝐵
4	3	sseli	⊢ ( 𝐴 ∈ Word ( 𝐵 ∩ 𝐶 ) → 𝐴 ∈ Word 𝐵 )
5		inss2	⊢ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐶
6		sswrd	⊢ ( ( 𝐵 ∩ 𝐶 ) ⊆ 𝐶 → Word ( 𝐵 ∩ 𝐶 ) ⊆ Word 𝐶 )
7	5 6	ax-mp	⊢ Word ( 𝐵 ∩ 𝐶 ) ⊆ Word 𝐶
8	7	sseli	⊢ ( 𝐴 ∈ Word ( 𝐵 ∩ 𝐶 ) → 𝐴 ∈ Word 𝐶 )
9	4 8	jca	⊢ ( 𝐴 ∈ Word ( 𝐵 ∩ 𝐶 ) → ( 𝐴 ∈ Word 𝐵 ∧ 𝐴 ∈ Word 𝐶 ) )