Definition df-s4 14867

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 14860	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14859	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14611	. . 3 class ⟨“𝐷”⟩
8		cconcat 14586	. . 3 class ++
9	6, 7, 8	co 7403	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1540	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14882  s4cld  14890  s4cli  14899  s4fv0  14912  s4fv1  14913  s4fv2  14914  s4fv3  14915  s4len  14916  s4prop  14927  s1s3  14941  s1s4  14942  s2s2  14946  s4s4  14949  s7rn  14982  tgcgr4  28456  konigsberglem1  30179  konigsberglem2  30180  konigsberglem3  30181  gpgprismgr4cycllem8  48049