Theorem wrdeq

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

	Ref	Expression
Assertion	wrdeq	⊢ ( 𝑆 = 𝑇 → Word 𝑆 = Word 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		sswrd	⊢ ( 𝑆 ⊆ 𝑇 → Word 𝑆 ⊆ Word 𝑇 )
2		sswrd	⊢ ( 𝑇 ⊆ 𝑆 → Word 𝑇 ⊆ Word 𝑆 )
3	1 2	anim12i	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ 𝑆 ) → ( Word 𝑆 ⊆ Word 𝑇 ∧ Word 𝑇 ⊆ Word 𝑆 ) )
4		eqss	⊢ ( 𝑆 = 𝑇 ↔ ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ 𝑆 ) )
5		eqss	⊢ ( Word 𝑆 = Word 𝑇 ↔ ( Word 𝑆 ⊆ Word 𝑇 ∧ Word 𝑇 ⊆ Word 𝑆 ) )
6	3 4 5	3imtr4i	⊢ ( 𝑆 = 𝑇 → Word 𝑆 = Word 𝑇 )