Definition df-s4 14816

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 14809	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14808	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14560	. . 3 class ⟨“𝐷”⟩
8		cconcat 14535	. . 3 class ++
9	6, 7, 8	co 7387	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1540	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14831  s4cld  14839  s4cli  14848  s4fv0  14861  s4fv1  14862  s4fv2  14863  s4fv3  14864  s4len  14865  s4prop  14876  s1s3  14890  s1s4  14891  s2s2  14895  s4s4  14898  s7rn  14931  tgcgr4  28458  konigsberglem1  30181  konigsberglem2  30182  konigsberglem3  30183  gpgprismgr4cycllem8  48092