Definition df-s3 14993

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 14986	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14985	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14735	. . 3 class ⟨“𝐶”⟩
7		cconcat 14708	. . 3 class ++
8	5, 6, 7	co 7418	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1570	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is used by:  s3eqd  15008  s3cld  15016  s3cli  15025  s3fv0  15035  s3fv1  15036  s3fv2  15037  s3len  15038  s3tpop  15053  s4prop  15054  s3co  15065  s1s2  15067  s1s3  15068  s2s2  15073  s4s3  15075  s3s4  15077  s3eqs2s1eq  15082  repsw3  15097  s3rn  15110  2pthon3v  30525  konigsberglem1  30846  konigsberglem2  30847  konigsberglem3  30848  numtowerdt  47885