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 13640
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 13633 . 2 class ⟨“𝐴𝐵𝐶”⟩
51, 2cs2 13632 . . 3 class ⟨“𝐴𝐵”⟩
63cs1 13326 . . 3 class ⟨“𝐶”⟩
7 cconcat 13325 . . 3 class ++
85, 6, 7co 6690 . 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
94, 8wceq 1523 1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s3eqd  13655  s3cld  13663  s3cli  13672  s3fv0  13682  s3fv1  13683  s3fv2  13684  s3len  13685  s3tpop  13700  s4prop  13701  s3co  13712  s1s2  13714  s1s3  13715  s2s2  13720  s4s3  13722  s3s4  13724  s3eqs2s1eq  13729  repsw3  13740  2pthon3v  26908  konigsberglem1  27230  konigsberglem2  27231  konigsberglem3  27232
  Copyright terms: Public domain W3C validator