Description: Two length 2 words are equal iff the corresponding singleton words consisting of their symbols are equal. (Contributed by Alexander van der Vekens, 24-Sep-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | s2eq2s1eq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-s2 | |
|
2 | 1 | a1i | |
3 | df-s2 | |
|
4 | 3 | a1i | |
5 | 2 4 | eqeq12d | |
6 | s1cl | |
|
7 | s1cl | |
|
8 | 6 7 | anim12i | |
9 | 8 | adantr | |
10 | s1cl | |
|
11 | s1cl | |
|
12 | 10 11 | anim12i | |
13 | 12 | adantl | |
14 | s1len | |
|
15 | s1len | |
|
16 | 14 15 | eqtr4i | |
17 | 16 | a1i | |
18 | ccatopth | |
|
19 | 9 13 17 18 | syl3anc | |
20 | 5 19 | bitrd | |