Definition df-s4 14773

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 14766	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14765	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14519	. . 3 class ⟨“𝐷”⟩
8		cconcat 14493	. . 3 class ++
9	6, 7, 8	co 7358	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1541	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14788  s4cld  14796  s4cli  14805  s4fv0  14818  s4fv1  14819  s4fv2  14820  s4fv3  14821  s4len  14822  s4prop  14833  s1s3  14847  s1s4  14848  s2s2  14852  s4s4  14855  s7rn  14888  tgcgr4  28603  konigsberglem1  30327  konigsberglem2  30328  konigsberglem3  30329  nthrucw  47130  gpgprismgr4cycllem8  48348