Definition df-s3 14800

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 14793	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14792	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14545	. . 3 class ⟨“𝐶”⟩
7		cconcat 14520	. . 3 class ++
8	5, 6, 7	co 7409	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1542	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14815  s3cld  14823  s3cli  14832  s3fv0  14842  s3fv1  14843  s3fv2  14844  s3len  14845  s3tpop  14860  s4prop  14861  s3co  14872  s1s2  14874  s1s3  14875  s2s2  14880  s4s3  14882  s3s4  14884  s3eqs2s1eq  14889  repsw3  14902  2pthon3v  29197  konigsberglem1  29505  konigsberglem2  29506  konigsberglem3  29507