Definition df-s4 14806

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 14799	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14798	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14552	. . 3 class ⟨“𝐷”⟩
8		cconcat 14526	. . 3 class ++
9	6, 7, 8	co 7361	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1542	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14821  s4cld  14829  s4cli  14838  s4fv0  14851  s4fv1  14852  s4fv2  14853  s4fv3  14854  s4len  14855  s4prop  14866  s1s3  14880  s1s4  14881  s2s2  14885  s4s4  14888  s7rn  14921  tgcgr4  28616  konigsberglem1  30340  konigsberglem2  30341  konigsberglem3  30342  nthrucw  47335  gpgprismgr4cycllem8  48593