Definition df-s3 14905

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 14898	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14897	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14647	. . 3 class ⟨“𝐶”⟩
7		cconcat 14620	. . 3 class ++
8	5, 6, 7	co 7416	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1570	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is used by:  s3eqd  14920  s3cld  14928  s3cli  14937  s3fv0  14947  s3fv1  14948  s3fv2  14949  s3len  14950  s3tpop  14965  s4prop  14966  s3co  14977  s1s2  14979  s1s3  14980  s2s2  14985  s4s3  14987  s3s4  14989  s3eqs2s1eq  14994  repsw3  15007  s3rn  15020  2pthon3v  30321  konigsberglem1  30632  konigsberglem2  30633  konigsberglem3  30634  nthrucw  47640