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 14888
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 14881 . 2 class ⟨“𝐴𝐵𝐶”⟩
51, 2cs2 14880 . . 3 class ⟨“𝐴𝐵”⟩
63cs1 14633 . . 3 class ⟨“𝐶”⟩
7 cconcat 14608 . . 3 class ++
85, 6, 7co 7431 . 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
94, 8wceq 1540 1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s3eqd  14903  s3cld  14911  s3cli  14920  s3fv0  14930  s3fv1  14931  s3fv2  14932  s3len  14933  s3tpop  14948  s4prop  14949  s3co  14960  s1s2  14962  s1s3  14963  s2s2  14968  s4s3  14970  s3s4  14972  s3eqs2s1eq  14977  repsw3  14990  s3rn  15003  2pthon3v  29963  konigsberglem1  30271  konigsberglem2  30272  konigsberglem3  30273
  Copyright terms: Public domain W3C validator