Definition df-s4 14823

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 14816	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14815	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14567	. . 3 class ⟨“𝐷”⟩
8		cconcat 14542	. . 3 class ++
9	6, 7, 8	co 7390	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1540	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14838  s4cld  14846  s4cli  14855  s4fv0  14868  s4fv1  14869  s4fv2  14870  s4fv3  14871  s4len  14872  s4prop  14883  s1s3  14897  s1s4  14898  s2s2  14902  s4s4  14905  s7rn  14938  tgcgr4  28465  konigsberglem1  30188  konigsberglem2  30189  konigsberglem3  30190  gpgprismgr4cycllem8  48096