Description: Equality theorem for the set of words. (Contributed by Mario Carneiro, 26-Feb-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | wrdeq | |- ( S = T -> Word S = Word T ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sswrd | |- ( S C_ T -> Word S C_ Word T ) |
|
2 | sswrd | |- ( T C_ S -> Word T C_ Word S ) |
|
3 | 1 2 | anim12i | |- ( ( S C_ T /\ T C_ S ) -> ( Word S C_ Word T /\ Word T C_ Word S ) ) |
4 | eqss | |- ( S = T <-> ( S C_ T /\ T C_ S ) ) |
|
5 | eqss | |- ( Word S = Word T <-> ( Word S C_ Word T /\ Word T C_ Word S ) ) |
|
6 | 3 4 5 | 3imtr4i | |- ( S = T -> Word S = Word T ) |