Definition df-s3 14490

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 14483	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14482	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14228	. . 3 class ⟨“𝐶”⟩
7		cconcat 14201	. . 3 class ++
8	5, 6, 7	co 7255	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1539	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14505  s3cld  14513  s3cli  14522  s3fv0  14532  s3fv1  14533  s3fv2  14534  s3len  14535  s3tpop  14550  s4prop  14551  s3co  14562  s1s2  14564  s1s3  14565  s2s2  14570  s4s3  14572  s3s4  14574  s3eqs2s1eq  14579  repsw3  14592  2pthon3v  28209  konigsberglem1  28517  konigsberglem2  28518  konigsberglem3  28519