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

Definition df-s3 13445
 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 13438 . 2 class ⟨“𝐴𝐵𝐶”⟩
51, 2cs2 13437 . . 3 class ⟨“𝐴𝐵”⟩
63cs1 13149 . . 3 class ⟨“𝐶”⟩
7 cconcat 13148 . . 3 class ++
85, 6, 7co 6549 . 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
94, 8wceq 1475 1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
 Colors of variables: wff setvar class This definition is referenced by:  s3eqd  13460  s3cld  13467  s3cli  13476  s3fv0  13486  s3fv1  13487  s3fv2  13488  s3len  13489  s3tpop  13504  s4prop  13505  s3co  13516  s1s2  13518  s1s3  13519  s2s2  13524  s4s3  13526  s3s4  13528  repsw3  13542  konigsberg  26514  2pthon3v-av  41150  konigsberglem1  41422  konigsberglem2  41423  konigsberglem3  41424
 Copyright terms: Public domain W3C validator