Metamath Proof Explorer

Theorem s3fv2

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

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

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 1 2 3 cats1fvn 
 |-  ( C e. V -> ( <" A B C "> ` 2 ) = C )