Definition df-s4 14785

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 14778	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14777	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14531	. . 3 class ⟨“𝐷”⟩
8		cconcat 14505	. . 3 class ++
9	6, 7, 8	co 7368	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1542	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14800  s4cld  14808  s4cli  14817  s4fv0  14830  s4fv1  14831  s4fv2  14832  s4fv3  14833  s4len  14834  s4prop  14845  s1s3  14859  s1s4  14860  s2s2  14864  s4s4  14867  s7rn  14900  tgcgr4  28615  konigsberglem1  30339  konigsberglem2  30340  konigsberglem3  30341  nthrucw  47244  gpgprismgr4cycllem8  48462