Metamath Proof Explorer

Theorem pfxwrdsymb

Description: A prefix of a word is a word over the symbols it consists of. (Contributed by AV, 3-Dec-2022)

		Ref	Expression
	Assertion	pfxwrdsymb	$⊢ S \in Word A \to S prefix L \in Word S [(0 ..^L)]$

Step	Hyp	Ref	Expression
1		pfxval0	$⊢ S \in Word A \to S prefix L = S substr ⟨0, L⟩$
2		swrdwrdsymb	$⊢ S \in Word A \to S substr ⟨0, L⟩ \in Word S [(0 ..^L)]$
3	1 2	eqeltrd	$⊢ S \in Word A \to S prefix L \in Word S [(0 ..^L)]$