Theorem s2fv1

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

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

Proof

Step	Hyp	Ref	Expression
1		df-s2	|- <" A B "> = ( <" A "> ++ <" B "> )
2		s1cli	|- <" A "> e. Word _V
3		s1len	|- ( # ` <" A "> ) = 1
4	1 2 3	cats1fvn	|- ( B e. V -> ( <" A B "> ` 1 ) = B )