Definition df-s4 13595

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 13588	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 13587	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 13294	. . 3 class ⟨“𝐷”⟩
8		cconcat 13293	. . 3 class ++
9	6, 7, 8	co 6650	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1483	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  13610  s4cld  13618  s4cli  13627  s4fv0  13640  s4fv1  13641  s4fv2  13642  s4fv3  13643  s4len  13644  s4prop  13655  s1s3  13669  s1s4  13670  s2s2  13674  s4s4  13677  tgcgr4  25426  konigsberglem1  27114  konigsberglem2  27115  konigsberglem3  27116