Definition df-s3 14884

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 14877	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14876	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14629	. . 3 class ⟨“𝐶”⟩
7		cconcat 14604	. . 3 class ++
8	5, 6, 7	co 7430	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1536	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14899  s3cld  14907  s3cli  14916  s3fv0  14926  s3fv1  14927  s3fv2  14928  s3len  14929  s3tpop  14944  s4prop  14945  s3co  14956  s1s2  14958  s1s3  14959  s2s2  14964  s4s3  14966  s3s4  14968  s3eqs2s1eq  14973  repsw3  14986  s3rn  14999  2pthon3v  29972  konigsberglem1  30280  konigsberglem2  30281  konigsberglem3  30282