Definition df-s4 14491

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 14484	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14483	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14228	. . 3 class ⟨“𝐷”⟩
8		cconcat 14201	. . 3 class ++
9	6, 7, 8	co 7255	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1539	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14506  s4cld  14514  s4cli  14523  s4fv0  14536  s4fv1  14537  s4fv2  14538  s4fv3  14539  s4len  14540  s4prop  14551  s1s3  14565  s1s4  14566  s2s2  14570  s4s4  14573  tgcgr4  26796  konigsberglem1  28517  konigsberglem2  28518  konigsberglem3  28519