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	⊢ 𝑆 ∈ V
Assertion	wrdexi	⊢ Word 𝑆 ∈ V

Proof

Step	Hyp	Ref	Expression
1		wrdexi.1	⊢ 𝑆 ∈ V
2		wrdexg	⊢ ( 𝑆 ∈ V → Word 𝑆 ∈ V )
3	1 2	ax-mp	⊢ Word 𝑆 ∈ V