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 13392
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 13385 . 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
61, 2, 3cs3 13384 . . 3 class ⟨“𝐴𝐵𝐶”⟩
74cs1 13095 . . 3 class ⟨“𝐷”⟩
8 cconcat 13094 . . 3 class ++
96, 7, 8co 6527 . 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
105, 9wceq 1474 1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s4eqd  13407  s4cld  13414  s4cli  13423  s4fv0  13436  s4fv1  13437  s4fv2  13438  s4fv3  13439  s4len  13440  s4prop  13451  s1s3  13465  s1s4  13466  s2s2  13470  s4s4  13473  tgcgr4  25144  usgraexmplvtx  25697  konigsberg  26280  konigsberglem1  41417  konigsberglem2  41418  konigsberglem3  41419
  Copyright terms: Public domain W3C validator