Theorem wrdeqi

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

	Ref	Expression
Hypothesis	wrdeqi.1	|- S = T
Assertion	wrdeqi	|- Word S = Word T

Proof

Step	Hyp	Ref	Expression
1		wrdeqi.1	|- S = T
2		wrdeq	|- ( S = T -> Word S = Word T )
3	1 2	ax-mp	|- Word S = Word T