Definition df-s3 14822

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 14815	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14814	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14567	. . 3 class ⟨“𝐶”⟩
7		cconcat 14542	. . 3 class ++
8	5, 6, 7	co 7390	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1540	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14837  s3cld  14845  s3cli  14854  s3fv0  14864  s3fv1  14865  s3fv2  14866  s3len  14867  s3tpop  14882  s4prop  14883  s3co  14894  s1s2  14896  s1s3  14897  s2s2  14902  s4s3  14904  s3s4  14906  s3eqs2s1eq  14911  repsw3  14924  s3rn  14937  2pthon3v  29880  konigsberglem1  30188  konigsberglem2  30189  konigsberglem3  30190