Definition df-s4 14869

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 14862	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14861	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14613	. . 3 class ⟨“𝐷”⟩
8		cconcat 14588	. . 3 class ++
9	6, 7, 8	co 7405	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1540	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14884  s4cld  14892  s4cli  14901  s4fv0  14914  s4fv1  14915  s4fv2  14916  s4fv3  14917  s4len  14918  s4prop  14929  s1s3  14943  s1s4  14944  s2s2  14948  s4s4  14951  s7rn  14984  tgcgr4  28510  konigsberglem1  30233  konigsberglem2  30234  konigsberglem3  30235  gpgprismgr4cycllem8  48101