Metamath Proof Explorer

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 \in Word (B \cap C) \to (A \in Word B \land A \in Word C)$

Proof

Step	Hyp	Ref	Expression
1		inss1	$⊢ B \cap C \subseteq B$
2		sswrd	$⊢ B \cap C \subseteq B \to Word (B \cap C) \subseteq Word B$
3	1 2	ax-mp	$⊢ Word (B \cap C) \subseteq Word B$
4	3	sseli	$⊢ A \in Word (B \cap C) \to A \in Word B$
5		inss2	$⊢ B \cap C \subseteq C$
6		sswrd	$⊢ B \cap C \subseteq C \to Word (B \cap C) \subseteq Word C$
7	5 6	ax-mp	$⊢ Word (B \cap C) \subseteq Word C$
8	7	sseli	$⊢ A \in Word (B \cap C) \to A \in Word C$
9	4 8	jca	$⊢ A \in Word (B \cap C) \to (A \in Word B \land A \in Word C)$