Definition df-s4 14887

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 14880	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14879	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14633	. . 3 class ⟨“𝐷”⟩
8		cconcat 14607	. . 3 class ++
9	6, 7, 8	co 7411	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1567	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14902  s4cld  14910  s4cli  14919  s4fv0  14932  s4fv1  14933  s4fv2  14934  s4fv3  14935  s4len  14936  s4prop  14947  s1s3  14961  s1s4  14962  s2s2  14966  s4s4  14969  s7rn  15002  tgcgr4  28766  konigsberglem1  30544  konigsberglem2  30545  konigsberglem3  30546  nthrucw  47494  gpgprismgr4cycllem8  48756