Theorem wrdeq

Description: Equality theorem for the set of words. (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Assertion	wrdeq	|- ( S = T -> Word S = Word T )

Proof

Step	Hyp	Ref	Expression
1		sswrd	|- ( S C_ T -> Word S C_ Word T )
2		sswrd	|- ( T C_ S -> Word T C_ Word S )
3	1 2	anim12i	|- ( ( S C_ T /\ T C_ S ) -> ( Word S C_ Word T /\ Word T C_ Word S ) )
4		eqss	|- ( S = T <-> ( S C_ T /\ T C_ S ) )
5		eqss	|- ( Word S = Word T <-> ( Word S C_ Word T /\ Word T C_ Word S ) )
6	3 4 5	3imtr4i	|- ( S = T -> Word S = Word T )