Definition df-s3 14807

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 14800	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14799	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14552	. . 3 class ⟨“𝐶”⟩
7		cconcat 14527	. . 3 class ++
8	5, 6, 7	co 7412	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1540	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14822  s3cld  14830  s3cli  14839  s3fv0  14849  s3fv1  14850  s3fv2  14851  s3len  14852  s3tpop  14867  s4prop  14868  s3co  14879  s1s2  14881  s1s3  14882  s2s2  14887  s4s3  14889  s3s4  14891  s3eqs2s1eq  14896  repsw3  14909  2pthon3v  29632  konigsberglem1  29940  konigsberglem2  29941  konigsberglem3  29942