Metamath Proof Explorer

Theorem s2fv0

Description: Extract the first symbol from a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s2fv0 
|- ( A e. V -> ( <" A B "> ` 0 ) = A )

Proof

Step Hyp Ref Expression
1 df-s2 
 |-  <" A B "> = ( <" A "> ++ <" B "> )
2 s1cli 
 |-  <" A "> e. Word _V
3 s1len 
 |-  ( # ` <" A "> ) = 1
4 s1fv 
 |-  ( A e. V -> ( <" A "> ` 0 ) = A )
5 0nn0 
 |-  0 e. NN0
6 0lt1 
 |-  0 < 1
7 1 2 3 4 5 6 cats1fv 
 |-  ( A e. V -> ( <" A B "> ` 0 ) = A )