Definition df-s4 14203

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 14196	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14195	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 13940	. . 3 class ⟨“𝐷”⟩
8		cconcat 13913	. . 3 class ++
9	6, 7, 8	co 7135	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1538	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14218  s4cld  14226  s4cli  14235  s4fv0  14248  s4fv1  14249  s4fv2  14250  s4fv3  14251  s4len  14252  s4prop  14263  s1s3  14277  s1s4  14278  s2s2  14282  s4s4  14285  tgcgr4  26325  konigsberglem1  28037  konigsberglem2  28038  konigsberglem3  28039