Theorem wrdexi

Description: The set of words over a set is a set, inference form. (Contributed by AV, 23-May-2021)

	Ref	Expression
Hypothesis	wrdexi.1	$$⊢S\in \mathrm{V}$$
Assertion	wrdexi	$$⊢\mathrm{Word}S\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		wrdexi.1	$$⊢S\in \mathrm{V}$$
2		wrdexg	$$⊢S\in \mathrm{V}\to \mathrm{Word}S\in \mathrm{V}$$
3	1 2	ax-mp	$$⊢\mathrm{Word}S\in \mathrm{V}$$