Definition df-s4 14771

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 14764	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14763	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14517	. . 3 class ⟨“𝐷”⟩
8		cconcat 14491	. . 3 class ++
9	6, 7, 8	co 7356	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1541	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14786  s4cld  14794  s4cli  14803  s4fv0  14816  s4fv1  14817  s4fv2  14818  s4fv3  14819  s4len  14820  s4prop  14831  s1s3  14845  s1s4  14846  s2s2  14850  s4s4  14853  s7rn  14886  tgcgr4  28552  konigsberglem1  30276  konigsberglem2  30277  konigsberglem3  30278  nthrucw  47072  gpgprismgr4cycllem8  48290