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 13892
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 13885 . 2 class ⟨“𝐴𝐵𝐶”⟩
51, 2cs2 13884 . . 3 class ⟨“𝐴𝐵”⟩
63cs1 13572 . . 3 class ⟨“𝐶”⟩
7 cconcat 13547 . . 3 class ++
85, 6, 7co 6846 . 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
94, 8wceq 1652 1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s3eqd  13907  s3cld  13915  s3cli  13924  s3fv0  13934  s3fv1  13935  s3fv2  13936  s3len  13937  s3tpop  13952  s4prop  13953  s3co  13964  s1s2  13966  s1s3  13967  s2s2  13972  s4s3  13974  s3s4  13976  s3eqs2s1eq  13981  repsw3  13994  2pthon3v  27184  konigsberglem1  27551  konigsberglem2  27552  konigsberglem3  27553
  Copyright terms: Public domain W3C validator