Metamath Proof Explorer


Theorem wrdeq

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 )

Proof

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 )