Definition df-s3 14797

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 14790	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14789	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14542	. . 3 class ⟨“𝐶”⟩
7		cconcat 14517	. . 3 class ++
8	5, 6, 7	co 7406	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1542	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14812  s3cld  14820  s3cli  14829  s3fv0  14839  s3fv1  14840  s3fv2  14841  s3len  14842  s3tpop  14857  s4prop  14858  s3co  14869  s1s2  14871  s1s3  14872  s2s2  14877  s4s3  14879  s3s4  14881  s3eqs2s1eq  14886  repsw3  14899  2pthon3v  29187  konigsberglem1  29495  konigsberglem2  29496  konigsberglem3  29497