Definition df-s4 13815

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 13808	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 13807	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 13500	. . 3 class ⟨“𝐷”⟩
8		cconcat 13499	. . 3 class ++
9	6, 7, 8	co 6814	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1632	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  13830  s4cld  13838  s4cli  13847  s4fv0  13860  s4fv1  13861  s4fv2  13862  s4fv3  13863  s4len  13864  s4prop  13875  s1s3  13889  s1s4  13890  s2s2  13894  s4s4  13897  tgcgr4  25646  konigsberglem1  27425  konigsberglem2  27426  konigsberglem3  27427