Metamath Proof Explorer


Theorem s3fv1

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

Ref Expression
Assertion s3fv1
|- ( B e. V -> ( <" A B C "> ` 1 ) = B )

Proof

Step Hyp Ref Expression
1 df-s3
 |-  <" A B C "> = ( <" A B "> ++ <" C "> )
2 s2cli
 |-  <" A B "> e. Word _V
3 s2len
 |-  ( # ` <" A B "> ) = 2
4 s2fv1
 |-  ( B e. V -> ( <" A B "> ` 1 ) = B )
5 1nn0
 |-  1 e. NN0
6 1lt2
 |-  1 < 2
7 1 2 3 4 5 6 cats1fv
 |-  ( B e. V -> ( <" A B C "> ` 1 ) = B )