Definition df-s3 13445

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 13438	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 13437	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 13149	. . 3 class ⟨“𝐶”⟩
7		cconcat 13148	. . 3 class ++
8	5, 6, 7	co 6549	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1475	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  13460  s3cld  13467  s3cli  13476  s3fv0  13486  s3fv1  13487  s3fv2  13488  s3len  13489  s3tpop  13504  s4prop  13505  s3co  13516  s1s2  13518  s1s3  13519  s2s2  13524  s4s3  13526  s3s4  13528  repsw3  13542  konigsberg  26514  2pthon3v-av  41150  konigsberglem1  41422  konigsberglem2  41423  konigsberglem3  41424