Definition df-s4 13795

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 13788	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 13787	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 13480	. . 3 class ⟨“𝐷”⟩
8		cconcat 13479	. . 3 class ++
9	6, 7, 8	co 6813	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1632	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  13810  s4cld  13818  s4cli  13827  s4fv0  13840  s4fv1  13841  s4fv2  13842  s4fv3  13843  s4len  13844  s4prop  13855  s1s3  13869  s1s4  13870  s2s2  13874  s4s4  13877  tgcgr4  25625  konigsberglem1  27404  konigsberglem2  27405  konigsberglem3  27406