Definition df-s4 14863

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 14856	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14855	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14609	. . 3 class ⟨“𝐷”⟩
8		cconcat 14583	. . 3 class ++
9	6, 7, 8	co 7396	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1560	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14878  s4cld  14886  s4cli  14895  s4fv0  14908  s4fv1  14909  s4fv2  14910  s4fv3  14911  s4len  14912  s4prop  14923  s1s3  14937  s1s4  14938  s2s2  14942  s4s4  14945  s7rn  14978  tgcgr4  28700  konigsberglem1  30454  konigsberglem2  30455  konigsberglem3  30456  nthrucw  47462  gpgprismgr4cycllem8  48724