Theorem wrdeqi

Description: Equality theorem for the set of words, inference form. (Contributed by AV, 23-May-2021)

	Ref	Expression
Hypothesis	wrdeqi.1	⊢ 𝑆 = 𝑇
Assertion	wrdeqi	⊢ Word 𝑆 = Word 𝑇

Proof

Step	Hyp	Ref	Expression
1		wrdeqi.1	⊢ 𝑆 = 𝑇
2		wrdeq	⊢ ( 𝑆 = 𝑇 → Word 𝑆 = Word 𝑇 )
3	1 2	ax-mp	⊢ Word 𝑆 = Word 𝑇