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 e. _V
Assertion	wrdexi	|- Word S e. _V

Proof

Step	Hyp	Ref	Expression
1		wrdexi.1	|- S e. _V
2		wrdexg	|- ( S e. _V -> Word S e. _V )
3	1 2	ax-mp	|- Word S e. _V