Definition df-s3 13391

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 13384	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 13383	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 13095	. . 3 class ⟨“𝐶”⟩
7		cconcat 13094	. . 3 class ++
8	5, 6, 7	co 6527	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1474	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  13406  s3cld  13413  s3cli  13422  s3fv0  13432  s3fv1  13433  s3fv2  13434  s3len  13435  s3tpop  13450  s4prop  13451  s3co  13462  s1s2  13464  s1s3  13465  s2s2  13470  s4s3  13472  s3s4  13474  repsw3  13488  konigsberg  26280  2pthon3v-av  41145  konigsberglem1  41417  konigsberglem2  41418  konigsberglem3  41419