MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-s4 Structured version   Visualization version   GIF version

Definition df-s4 14797
Description: Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
df-s4 ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

Detailed syntax breakdown of Definition df-s4
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cC . . 3 class 𝐶
4 cD . . 3 class 𝐷
51, 2, 3, 4cs4 14790 . 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
61, 2, 3cs3 14789 . . 3 class ⟨“𝐴𝐵𝐶”⟩
74cs1 14541 . . 3 class ⟨“𝐷”⟩
8 cconcat 14516 . . 3 class ++
96, 7, 8co 7401 . 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
105, 9wceq 1533 1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s4eqd  14812  s4cld  14820  s4cli  14829  s4fv0  14842  s4fv1  14843  s4fv2  14844  s4fv3  14845  s4len  14846  s4prop  14857  s1s3  14871  s1s4  14872  s2s2  14876  s4s4  14879  tgcgr4  28206  konigsberglem1  29929  konigsberglem2  29930  konigsberglem3  29931
  Copyright terms: Public domain W3C validator