Metamath Proof Explorer

Theorem wrdv

Description: A word over an alphabet is a word over the universal class. (Contributed by AV, 8-Feb-2021) (Proof shortened by JJ, 18-Nov-2022)

Ref Expression
Assertion wrdv 
|- ( W e. Word V -> W e. Word _V )

Proof

Step Hyp Ref Expression
1 ssv 
 |-  V C_ _V
2 sswrd 
 |-  ( V C_ _V -> Word V C_ Word _V )
3 1 2 ax-mp 
 |-  Word V C_ Word _V
4 3 sseli 
 |-  ( W e. Word V -> W e. Word _V )