| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-s3 | Structured version Visualization version GIF version | ||
| Description: Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
| Ref | Expression |
|---|---|
| df-s3 | ⊢ 〈“𝐴𝐵𝐶”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | cB | . . 3 class 𝐵 | |
| 3 | cC | . . 3 class 𝐶 | |
| 4 | 1, 2, 3 | cs3 14881 | . 2 class 〈“𝐴𝐵𝐶”〉 |
| 5 | 1, 2 | cs2 14880 | . . 3 class 〈“𝐴𝐵”〉 |
| 6 | 3 | cs1 14633 | . . 3 class 〈“𝐶”〉 |
| 7 | cconcat 14608 | . . 3 class ++ | |
| 8 | 5, 6, 7 | co 7431 | . 2 class (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) |
| 9 | 4, 8 | wceq 1540 | 1 wff 〈“𝐴𝐵𝐶”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) |
| Colors of variables: wff setvar class |
| This definition is referenced by: s3eqd 14903 s3cld 14911 s3cli 14920 s3fv0 14930 s3fv1 14931 s3fv2 14932 s3len 14933 s3tpop 14948 s4prop 14949 s3co 14960 s1s2 14962 s1s3 14963 s2s2 14968 s4s3 14970 s3s4 14972 s3eqs2s1eq 14977 repsw3 14990 s3rn 15003 2pthon3v 29963 konigsberglem1 30271 konigsberglem2 30272 konigsberglem3 30273 |
| Copyright terms: Public domain | W3C validator |