Definition df-s4 14792

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 14785	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14784	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14536	. . 3 class ⟨“𝐷”⟩
8		cconcat 14511	. . 3 class ++
9	6, 7, 8	co 7369	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1540	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14807  s4cld  14815  s4cli  14824  s4fv0  14837  s4fv1  14838  s4fv2  14839  s4fv3  14840  s4len  14841  s4prop  14852  s1s3  14866  s1s4  14867  s2s2  14871  s4s4  14874  s7rn  14907  tgcgr4  28511  konigsberglem1  30231  konigsberglem2  30232  konigsberglem3  30233  gpgprismgr4cycllem8  48085