| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-s4 | Structured version Visualization version GIF version | ||
| Description: Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
| Ref | Expression |
|---|---|
| df-s4 | ⊢ 〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | cB | . . 3 class 𝐵 | |
| 3 | cC | . . 3 class 𝐶 | |
| 4 | cD | . . 3 class 𝐷 | |
| 5 | 1, 2, 3, 4 | cs4 14882 | . 2 class 〈“𝐴𝐵𝐶𝐷”〉 |
| 6 | 1, 2, 3 | cs3 14881 | . . 3 class 〈“𝐴𝐵𝐶”〉 |
| 7 | 4 | cs1 14633 | . . 3 class 〈“𝐷”〉 |
| 8 | cconcat 14608 | . . 3 class ++ | |
| 9 | 6, 7, 8 | co 7431 | . 2 class (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) |
| 10 | 5, 9 | wceq 1540 | 1 wff 〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) |
| Colors of variables: wff setvar class |
| This definition is referenced by: s4eqd 14904 s4cld 14912 s4cli 14921 s4fv0 14934 s4fv1 14935 s4fv2 14936 s4fv3 14937 s4len 14938 s4prop 14949 s1s3 14963 s1s4 14964 s2s2 14968 s4s4 14971 s7rn 15004 tgcgr4 28539 konigsberglem1 30271 konigsberglem2 30272 konigsberglem3 30273 |
| Copyright terms: Public domain | W3C validator |