pfxval

		Ref	Expression
	Assertion	pfxval	$⊢ (S \in V \land L \in ℕ_{0}) \to S prefix L = S substr ⟨0, L⟩$

Step	Hyp	Ref	Expression
1		df-pfx	$⊢ prefix = (s \in V, l \in ℕ_{0} ⟼ s substr ⟨0, l⟩)$
2	1	a1i	$⊢ (S \in V \land L \in ℕ_{0}) \to prefix = (s \in V, l \in ℕ_{0} ⟼ s substr ⟨0, l⟩)$
3		simpl	$⊢ (s = S \land l = L) \to s = S$
4		opeq2	$⊢ l = L \to ⟨0, l⟩ = ⟨0, L⟩$
5	4	adantl	$⊢ (s = S \land l = L) \to ⟨0, l⟩ = ⟨0, L⟩$
6	3 5	oveq12d	$⊢ (s = S \land l = L) \to s substr ⟨0, l⟩ = S substr ⟨0, L⟩$
7	6	adantl	$⊢ ((S \in V \land L \in ℕ_{0}) \land (s = S \land l = L)) \to s substr ⟨0, l⟩ = S substr ⟨0, L⟩$
8		elex	$⊢ S \in V \to S \in V$
9	8	adantr	$⊢ (S \in V \land L \in ℕ_{0}) \to S \in V$
10		simpr	$⊢ (S \in V \land L \in ℕ_{0}) \to L \in ℕ_{0}$
11		ovexd	$⊢ (S \in V \land L \in ℕ_{0}) \to S substr ⟨0, L⟩ \in V$
12	2 7 9 10 11	ovmpod	$⊢ (S \in V \land L \in ℕ_{0}) \to S prefix L = S substr ⟨0, L⟩$

Metamath Proof Explorer