Definition df-s4 14883

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 14876	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14875	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14629	. . 3 class ⟨“𝐷”⟩
8		cconcat 14603	. . 3 class ++
9	6, 7, 8	co 7410	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1570	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14898  s4cld  14906  s4cli  14915  s4fv0  14928  s4fv1  14929  s4fv2  14930  s4fv3  14931  s4len  14932  s4prop  14943  s1s3  14957  s1s4  14958  s2s2  14962  s4s4  14965  s7rn  14998  tgcgr4  28800  konigsberglem1  30603  konigsberglem2  30604  konigsberglem3  30605  nthrucw  47627  gpgprismgr4cycllem8  48887