Definition df-s4 14798

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 14791	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14790	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14542	. . 3 class ⟨“𝐷”⟩
8		cconcat 14517	. . 3 class ++
9	6, 7, 8	co 7406	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1542	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14813  s4cld  14821  s4cli  14830  s4fv0  14843  s4fv1  14844  s4fv2  14845  s4fv3  14846  s4len  14847  s4prop  14858  s1s3  14872  s1s4  14873  s2s2  14877  s4s4  14880  tgcgr4  27772  konigsberglem1  29495  konigsberglem2  29496  konigsberglem3  29497