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 14203
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 14196 . 2 class ⟨“𝐴𝐵𝐶”⟩
51, 2cs2 14195 . . 3 class ⟨“𝐴𝐵”⟩
63cs1 13941 . . 3 class ⟨“𝐶”⟩
7 cconcat 13914 . . 3 class ++
85, 6, 7co 7148 . 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
94, 8wceq 1531 1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s3eqd  14218  s3cld  14226  s3cli  14235  s3fv0  14245  s3fv1  14246  s3fv2  14247  s3len  14248  s3tpop  14263  s4prop  14264  s3co  14275  s1s2  14277  s1s3  14278  s2s2  14283  s4s3  14285  s3s4  14287  s3eqs2s1eq  14292  repsw3  14305  2pthon3v  27714  konigsberglem1  28023  konigsberglem2  28024  konigsberglem3  28025
  Copyright terms: Public domain W3C validator