Definition df-s3 15042

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 15035	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 15034	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14783	. . 3 class ⟨“𝐶”⟩
7		cconcat 14756	. . 3 class ++
8	5, 6, 7	co 7451	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1570	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is used by:  s3eqd  15057  s3cld  15065  s3cli  15074  s3fv0  15085  s3fv1  15086  s3fv2  15087  s3len  15088  s3tpop  15103  s4prop  15104  s3co  15115  s1s2  15117  s1s3  15118  s2s2  15123  s4s3  15125  s3s4  15127  s3eqs2s1eq  15132  repsw3  15147  s3rn  15160  2pthon3v  30589  konigsberglem1  30910  konigsberglem2  30911  konigsberglem3  30912  numtowerdt  48189