Definition df-s4 15001

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 14994	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14993	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14742	. . 3 class ⟨“𝐷”⟩
8		cconcat 14715	. . 3 class ++
9	6, 7, 8	co 7420	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1570	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is used by:  s4eqd  15016  s4cld  15024  s4cli  15033  s4fv0  15046  s4fv1  15047  s4fv2  15048  s4fv3  15049  s4len  15050  s4prop  15061  s1s3  15075  s1s4  15076  s2s2  15080  s4s4  15083  s7rn  15118  tgcgr4  28994  konigsberglem1  30853  konigsberglem2  30854  konigsberglem3  30855  numtowerdt  47915  gpgprismgr4cycllem8  49199