Definition df-s4 14899

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 14892	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14891	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14643	. . 3 class ⟨“𝐷”⟩
8		cconcat 14618	. . 3 class ++
9	6, 7, 8	co 7448	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1537	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14914  s4cld  14922  s4cli  14931  s4fv0  14944  s4fv1  14945  s4fv2  14946  s4fv3  14947  s4len  14948  s4prop  14959  s1s3  14973  s1s4  14974  s2s2  14978  s4s4  14981  s7rn  15014  tgcgr4  28557  konigsberglem1  30284  konigsberglem2  30285  konigsberglem3  30286