Definition df-s3 14898

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 14891	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14890	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14643	. . 3 class ⟨“𝐶”⟩
7		cconcat 14618	. . 3 class ++
8	5, 6, 7	co 7448	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1537	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14913  s3cld  14921  s3cli  14930  s3fv0  14940  s3fv1  14941  s3fv2  14942  s3len  14943  s3tpop  14958  s4prop  14959  s3co  14970  s1s2  14972  s1s3  14973  s2s2  14978  s4s3  14980  s3s4  14982  s3eqs2s1eq  14987  repsw3  15000  s3rn  15013  2pthon3v  29976  konigsberglem1  30284  konigsberglem2  30285  konigsberglem3  30286