Definition df-s4 14922

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 14915	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14914	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14663	. . 3 class ⟨“𝐷”⟩
8		cconcat 14636	. . 3 class ++
9	6, 7, 8	co 7414	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1570	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is used by:  s4eqd  14937  s4cld  14945  s4cli  14954  s4fv0  14967  s4fv1  14968  s4fv2  14969  s4fv3  14970  s4len  14971  s4prop  14982  s1s3  14996  s1s4  14997  s2s2  15001  s4s4  15004  s7rn  15039  tgcgr4  28874  konigsberglem1  30733  konigsberglem2  30734  konigsberglem3  30735  numtowerdt  47735  gpgprismgr4cycllem8  49019