Definition df-s3 13640

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 13633	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 13632	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 13326	. . 3 class ⟨“𝐶”⟩
7		cconcat 13325	. . 3 class ++
8	5, 6, 7	co 6690	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1523	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  13655  s3cld  13663  s3cli  13672  s3fv0  13682  s3fv1  13683  s3fv2  13684  s3len  13685  s3tpop  13700  s4prop  13701  s3co  13712  s1s2  13714  s1s3  13715  s2s2  13720  s4s3  13722  s3s4  13724  s3eqs2s1eq  13729  repsw3  13740  2pthon3v  26908  konigsberglem1  27230  konigsberglem2  27231  konigsberglem3  27232