Definition df-s3 14753

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 14746	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14745	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14500	. . 3 class ⟨“𝐶”⟩
7		cconcat 14474	. . 3 class ++
8	5, 6, 7	co 7346	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1541	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14768  s3cld  14776  s3cli  14785  s3fv0  14795  s3fv1  14796  s3fv2  14797  s3len  14798  s3tpop  14813  s4prop  14814  s3co  14825  s1s2  14827  s1s3  14828  s2s2  14833  s4s3  14835  s3s4  14837  s3eqs2s1eq  14842  repsw3  14855  s3rn  14868  2pthon3v  29919  konigsberglem1  30227  konigsberglem2  30228  konigsberglem3  30229