Definition df-s4 14812

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 14805	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14804	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14558	. . 3 class ⟨“𝐷”⟩
8		cconcat 14532	. . 3 class ++
9	6, 7, 8	co 7367	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1542	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14827  s4cld  14835  s4cli  14844  s4fv0  14857  s4fv1  14858  s4fv2  14859  s4fv3  14860  s4len  14861  s4prop  14872  s1s3  14886  s1s4  14887  s2s2  14891  s4s4  14894  s7rn  14927  tgcgr4  28599  konigsberglem1  30322  konigsberglem2  30323  konigsberglem3  30324  nthrucw  47316  gpgprismgr4cycllem8  48578