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 ) |
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 ) |