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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wrdexi.1 | ⊢ 𝑆 ∈ V | |
2 | wrdexg | ⊢ ( 𝑆 ∈ V → Word 𝑆 ∈ V ) | |
3 | 1 2 | ax-mp | ⊢ Word 𝑆 ∈ V |