Definition df-s3 14923

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 14916	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14915	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14665	. . 3 class ⟨“𝐶”⟩
7		cconcat 14638	. . 3 class ++
8	5, 6, 7	co 7414	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1570	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is used by:  s3eqd  14938  s3cld  14946  s3cli  14955  s3fv0  14965  s3fv1  14966  s3fv2  14967  s3len  14968  s3tpop  14983  s4prop  14984  s3co  14995  s1s2  14997  s1s3  14998  s2s2  15003  s4s3  15005  s3s4  15007  s3eqs2s1eq  15012  repsw3  15027  s3rn  15040  2pthon3v  30414  konigsberglem1  30735  konigsberglem2  30736  konigsberglem3  30737  numtowerdt  47737