Definition df-s4 14757

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 14750	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 14749	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 14502	. . 3 class ⟨“𝐷”⟩
8		cconcat 14477	. . 3 class ++
9	6, 7, 8	co 7349	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1540	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  14772  s4cld  14780  s4cli  14789  s4fv0  14802  s4fv1  14803  s4fv2  14804  s4fv3  14805  s4len  14806  s4prop  14817  s1s3  14831  s1s4  14832  s2s2  14836  s4s4  14839  s7rn  14872  tgcgr4  28476  konigsberglem1  30196  konigsberglem2  30197  konigsberglem3  30198  gpgprismgr4cycllem8  48090