Metamath Proof Explorer


Theorem wrdsymb

Description: A word is a word over the symbols it consists of. (Contributed by AV, 1-Dec-2022)

Ref Expression
Assertion wrdsymb SWordASWordS0..^S

Proof

Step Hyp Ref Expression
1 wrdf SWordAS:0..^SA
2 fimadmfo S:0..^SAS:0..^SontoS0..^S
3 fof S:0..^SontoS0..^SS:0..^SS0..^S
4 1 2 3 3syl SWordAS:0..^SS0..^S
5 iswrdb SWordS0..^SS:0..^SS0..^S
6 4 5 sylibr SWordASWordS0..^S