Metamath Proof Explorer

Theorem s4fv3

Description: Extract the fourth symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020)

Ref Expression
Assertion s4fv3 
|- ( D e. V -> ( <" A B C D "> ` 3 ) = D )

Proof

Step Hyp Ref Expression
1 df-s4 
 |-  <" A B C D "> = ( <" A B C "> ++ <" D "> )
2 s3cli 
 |-  <" A B C "> e. Word _V
3 s3len 
 |-  ( # ` <" A B C "> ) = 3
4 1 2 3 cats1fvn 
 |-  ( D e. V -> ( <" A B C D "> ` 3 ) = D )