Metamath Proof Explorer


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