Definition df-s3 14202

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 14195	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14194	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 13940	. . 3 class ⟨“𝐶”⟩
7		cconcat 13913	. . 3 class ++
8	5, 6, 7	co 7135	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1538	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14217  s3cld  14225  s3cli  14234  s3fv0  14244  s3fv1  14245  s3fv2  14246  s3len  14247  s3tpop  14262  s4prop  14263  s3co  14274  s1s2  14276  s1s3  14277  s2s2  14282  s4s3  14284  s3s4  14286  s3eqs2s1eq  14291  repsw3  14304  2pthon3v  27729  konigsberglem1  28037  konigsberglem2  28038  konigsberglem3  28039