Definition df-s3 14920

Description: Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)

Assertion

Ref	Expression
df-s3	⊢ ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

Detailed syntax breakdown of Definition df-s3

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cC	. . 3 class 𝐶
4	1, 2, 3	cs3 14913	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14912	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14662	. . 3 class ⟨“𝐶”⟩
7		cconcat 14635	. . 3 class ++
8	5, 6, 7	co 7413	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1570	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is used by:  s3eqd  14935  s3cld  14943  s3cli  14952  s3fv0  14962  s3fv1  14963  s3fv2  14964  s3len  14965  s3tpop  14980  s4prop  14981  s3co  14992  s1s2  14994  s1s3  14995  s2s2  15000  s4s3  15002  s3s4  15004  s3eqs2s1eq  15009  repsw3  15024  s3rn  15037  2pthon3v  30411  konigsberglem1  30732  konigsberglem2  30733  konigsberglem3  30734  numtowerdt  47734