Definition df-s3 14866

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 14859	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14858	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14611	. . 3 class ⟨“𝐶”⟩
7		cconcat 14586	. . 3 class ++
8	5, 6, 7	co 7403	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1540	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is referenced by:  s3eqd  14881  s3cld  14889  s3cli  14898  s3fv0  14908  s3fv1  14909  s3fv2  14910  s3len  14911  s3tpop  14926  s4prop  14927  s3co  14938  s1s2  14940  s1s3  14941  s2s2  14946  s4s3  14948  s3s4  14950  s3eqs2s1eq  14955  repsw3  14968  s3rn  14981  2pthon3v  29871  konigsberglem1  30179  konigsberglem2  30180  konigsberglem3  30181