Definition df-s3 14214

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 14207	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14206	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 13952	. . 3 class ⟨“𝐶”⟩
7		cconcat 13925	. . 3 class ++
8	5, 6, 7	co 7159	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1536	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14229  s3cld  14237  s3cli  14246  s3fv0  14256  s3fv1  14257  s3fv2  14258  s3len  14259  s3tpop  14274  s4prop  14275  s3co  14286  s1s2  14288  s1s3  14289  s2s2  14294  s4s3  14296  s3s4  14298  s3eqs2s1eq  14303  repsw3  14316  2pthon3v  27725  konigsberglem1  28034  konigsberglem2  28035  konigsberglem3  28036