Definition df-s4 14801

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 14794	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14793	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14545	. . 3 class ⟨“𝐷”⟩
8		cconcat 14520	. . 3 class ++
9	6, 7, 8	co 7409	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1542	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14816  s4cld  14824  s4cli  14833  s4fv0  14846  s4fv1  14847  s4fv2  14848  s4fv3  14849  s4len  14850  s4prop  14861  s1s3  14875  s1s4  14876  s2s2  14880  s4s4  14883  tgcgr4  27782  konigsberglem1  29505  konigsberglem2  29506  konigsberglem3  29507