Definition df-s4 15043

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 15036	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 15035	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14783	. . 3 class ⟨“𝐷”⟩
8		cconcat 14756	. . 3 class ++
9	6, 7, 8	co 7451	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1570	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is used by:  s4eqd  15058  s4cld  15066  s4cli  15075  s4fv0  15089  s4fv1  15090  s4fv2  15091  s4fv3  15092  s4len  15093  s4prop  15104  s1s3  15118  s1s4  15119  s2s2  15123  s4s4  15126  s7rn  15161  tgcgr4  29051  konigsberglem1  30910  konigsberglem2  30911  konigsberglem3  30912  numtowerdt  48189  gpgprismgr4cycllem8  49473