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 13391
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 13384 . 2 class ⟨“𝐴𝐵𝐶”⟩
51, 2cs2 13383 . . 3 class ⟨“𝐴𝐵”⟩
63cs1 13095 . . 3 class ⟨“𝐶”⟩
7 cconcat 13094 . . 3 class ++
85, 6, 7co 6527 . 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
94, 8wceq 1474 1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s3eqd  13406  s3cld  13413  s3cli  13422  s3fv0  13432  s3fv1  13433  s3fv2  13434  s3len  13435  s3tpop  13450  s4prop  13451  s3co  13462  s1s2  13464  s1s3  13465  s2s2  13470  s4s3  13472  s3s4  13474  repsw3  13488  konigsberg  26280  2pthon3v-av  41145  konigsberglem1  41417  konigsberglem2  41418  konigsberglem3  41419
  Copyright terms: Public domain W3C validator