Definition df-s3 14874

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 14867	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14866	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14621	. . 3 class ⟨“𝐶”⟩
7		cconcat 14595	. . 3 class ++
8	5, 6, 7	co 7400	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1563	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14889  s3cld  14897  s3cli  14906  s3fv0  14916  s3fv1  14917  s3fv2  14918  s3len  14919  s3tpop  14934  s4prop  14935  s3co  14946  s1s2  14948  s1s3  14949  s2s2  14954  s4s3  14956  s3s4  14958  s3eqs2s1eq  14963  repsw3  14976  s3rn  14989  2pthon3v  30197  konigsberglem1  30508  konigsberglem2  30509  konigsberglem3  30510  nthrucw  47461