Definition df-s4 14797

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 14790	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14789	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14541	. . 3 class ⟨“𝐷”⟩
8		cconcat 14516	. . 3 class ++
9	6, 7, 8	co 7401	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1533	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14812  s4cld  14820  s4cli  14829  s4fv0  14842  s4fv1  14843  s4fv2  14844  s4fv3  14845  s4len  14846  s4prop  14857  s1s3  14871  s1s4  14872  s2s2  14876  s4s4  14879  tgcgr4  28206  konigsberglem1  29929  konigsberglem2  29930  konigsberglem3  29931