Definition df-s4 15009

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 15002	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 15001	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14749	. . 3 class ⟨“𝐷”⟩
8		cconcat 14722	. . 3 class ++
9	6, 7, 8	co 7424	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1569	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is used by:  s4eqd  15024  s4cld  15032  s4cli  15041  s4fv0  15055  s4fv1  15056  s4fv2  15057  s4fv3  15058  s4len  15059  s4prop  15070  s1s3  15084  s1s4  15085  s2s2  15089  s4s4  15092  s7rn  15127  tgcgr4  29003  konigsberglem1  30862  konigsberglem2  30863  konigsberglem3  30864  numtowerdt  48052  gpgprismgr4cycllem8  49336