Definition df-s3 14211

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 14204	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14203	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 13949	. . 3 class ⟨“𝐶”⟩
7		cconcat 13922	. . 3 class ++
8	5, 6, 7	co 7156	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1537	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14226  s3cld  14234  s3cli  14243  s3fv0  14253  s3fv1  14254  s3fv2  14255  s3len  14256  s3tpop  14271  s4prop  14272  s3co  14283  s1s2  14285  s1s3  14286  s2s2  14291  s4s3  14293  s3s4  14295  s3eqs2s1eq  14300  repsw3  14313  2pthon3v  27722  konigsberglem1  28031  konigsberglem2  28032  konigsberglem3  28033