Definition df-s4 14913

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 14906	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14905	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14654	. . 3 class ⟨“𝐷”⟩
8		cconcat 14627	. . 3 class ++
9	6, 7, 8	co 7419	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1570	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is used by:  s4eqd  14928  s4cld  14936  s4cli  14945  s4fv0  14958  s4fv1  14959  s4fv2  14960  s4fv3  14961  s4len  14962  s4prop  14973  s1s3  14987  s1s4  14988  s2s2  14992  s4s4  14995  s7rn  15028  tgcgr4  28853  konigsberglem1  30676  konigsberglem2  30677  konigsberglem3  30678  nthrucw  47667  gpgprismgr4cycllem8  48927