Definition df-s4 14803

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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cC	. . 3 class 𝐶
4		cD	. . 3 class 𝐷
5	1, 2, 3, 4	cs4 14796	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14795	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14549	. . 3 class ⟨“𝐷”⟩
8		cconcat 14523	. . 3 class ++
9	6, 7, 8	co 7356	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1547	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14818  s4cld  14826  s4cli  14835  s4fv0  14848  s4fv1  14849  s4fv2  14850  s4fv3  14851  s4len  14852  s4prop  14863  s1s3  14877  s1s4  14878  s2s2  14882  s4s4  14885  s7rn  14918  tgcgr4  28617  konigsberglem1  30340  konigsberglem2  30341  konigsberglem3  30342  nthrucw  47331  gpgprismgr4cycllem8  48593