MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-s3 Structured version   Visualization version   GIF version

Definition df-s3 14201
Description: Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
df-s3 ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

Detailed syntax breakdown of Definition df-s3
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cC . . 3 class 𝐶
41, 2, 3cs3 14194 . 2 class ⟨“𝐴𝐵𝐶”⟩
51, 2cs2 14193 . . 3 class ⟨“𝐴𝐵”⟩
63cs1 13939 . . 3 class ⟨“𝐶”⟩
7 cconcat 13912 . . 3 class ++
85, 6, 7co 7145 . 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
94, 8wceq 1528 1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s3eqd  14216  s3cld  14224  s3cli  14233  s3fv0  14243  s3fv1  14244  s3fv2  14245  s3len  14246  s3tpop  14261  s4prop  14262  s3co  14273  s1s2  14275  s1s3  14276  s2s2  14281  s4s3  14283  s3s4  14285  s3eqs2s1eq  14290  repsw3  14303  2pthon3v  27650  konigsberglem1  27959  konigsberglem2  27960  konigsberglem3  27961
  Copyright terms: Public domain W3C validator