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	$$⊢\mathrm{Word}S=\mathrm{Word}T$$

Proof

Step	Hyp	Ref	Expression
1		wrdeqi.1	$$⊢S=T$$
2		wrdeq	$$⊢S=T\to \mathrm{Word}S=\mathrm{Word}T$$
3	1 2	ax-mp	$$⊢\mathrm{Word}S=\mathrm{Word}T$$