Definition df-s4 14563

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 14556	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14555	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14300	. . 3 class ⟨“𝐷”⟩
8		cconcat 14273	. . 3 class ++
9	6, 7, 8	co 7275	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1539	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14578  s4cld  14586  s4cli  14595  s4fv0  14608  s4fv1  14609  s4fv2  14610  s4fv3  14611  s4len  14612  s4prop  14623  s1s3  14637  s1s4  14638  s2s2  14642  s4s4  14645  tgcgr4  26892  konigsberglem1  28616  konigsberglem2  28617  konigsberglem3  28618