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 13794
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 13787 . 2 class ⟨“𝐴𝐵𝐶”⟩
51, 2cs2 13786 . . 3 class ⟨“𝐴𝐵”⟩
63cs1 13480 . . 3 class ⟨“𝐶”⟩
7 cconcat 13479 . . 3 class ++
85, 6, 7co 6813 . 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
94, 8wceq 1632 1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s3eqd  13809  s3cld  13817  s3cli  13826  s3fv0  13836  s3fv1  13837  s3fv2  13838  s3len  13839  s3tpop  13854  s4prop  13855  s3co  13866  s1s2  13868  s1s3  13869  s2s2  13874  s4s3  13876  s3s4  13878  s3eqs2s1eq  13883  repsw3  13895  2pthon3v  27063  konigsberglem1  27404  konigsberglem2  27405  konigsberglem3  27406
  Copyright terms: Public domain W3C validator