Definition df-s4 14885

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 14878	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14877	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14629	. . 3 class ⟨“𝐷”⟩
8		cconcat 14604	. . 3 class ++
9	6, 7, 8	co 7430	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1536	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14900  s4cld  14908  s4cli  14917  s4fv0  14930  s4fv1  14931  s4fv2  14932  s4fv3  14933  s4len  14934  s4prop  14945  s1s3  14959  s1s4  14960  s2s2  14964  s4s4  14967  s7rn  15000  tgcgr4  28553  konigsberglem1  30280  konigsberglem2  30281  konigsberglem3  30282