| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-s2 | Structured version Visualization version GIF version | ||
| Description: Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
| Ref | Expression |
|---|---|
| df-s2 | ⊢ 〈“𝐴𝐵”〉 = (〈“𝐴”〉 ++ 〈“𝐵”〉) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | cB | . . 3 class 𝐵 | |
| 3 | 1, 2 | cs2 14880 | . 2 class 〈“𝐴𝐵”〉 |
| 4 | 1 | cs1 14633 | . . 3 class 〈“𝐴”〉 |
| 5 | 2 | cs1 14633 | . . 3 class 〈“𝐵”〉 |
| 6 | cconcat 14608 | . . 3 class ++ | |
| 7 | 4, 5, 6 | co 7431 | . 2 class (〈“𝐴”〉 ++ 〈“𝐵”〉) |
| 8 | 3, 7 | wceq 1540 | 1 wff 〈“𝐴𝐵”〉 = (〈“𝐴”〉 ++ 〈“𝐵”〉) |
| Colors of variables: wff setvar class |
| This definition is referenced by: cats2cat 14901 s2eqd 14902 s2cld 14910 s2cli 14919 s2fv0 14926 s2fv1 14927 s2len 14928 s2prop 14946 s2co 14959 s1s2 14962 s2s2 14968 s4s2 14969 s2s5 14973 s5s2 14974 s2eq2s1eq 14975 swrds2 14979 repsw2 14989 ccatw2s1ccatws2 14993 s2rn 15002 ofs2 15010 gsumws2 18855 efginvrel2 19745 efgredlemc 19763 frgpnabllem1 19891 2pthon3v 29963 konigsberglem1 30271 konigsberglem2 30272 konigsberglem3 30273 cshw1s2 32945 ofcs2 34560 |
| Copyright terms: Public domain | W3C validator |