This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem s3fv0

Description: Extract the first symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017)

		Ref	Expression
	Assertion	s3fv0	$⊢ A \in V \to ⟨“ A B C ”⟩ (0) = A$

Step	Hyp	Ref	Expression
1		df-s3	$⊢ ⟨“ A B C ”⟩ = ⟨“ A B ”⟩ ++ ⟨“ C ”⟩$
2		s2cli	$⊢ ⟨“ A B ”⟩ \in Word V$
3		s2len	$⊢ \|⟨“ A B ”⟩\| = 2$
4		s2fv0	$⊢ A \in V \to ⟨“ A B ”⟩ (0) = A$
5		0nn0	$⊢ 0 \in ℕ_{0}$
6		2pos	$⊢ 0 < 2$
7	1 2 3 4 5 6	cats1fv	$⊢ A \in V \to ⟨“ A B C ”⟩ (0) = A$