Definition df-s3 15005

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 14998	. 2 class ⟨“𝐴𝐵𝐶”⟩
5	1, 2	cs2 14997	. . 3 class ⟨“𝐴𝐵”⟩
6	3	cs1 14746	. . 3 class ⟨“𝐶”⟩
7		cconcat 14719	. . 3 class ++
8	5, 6, 7	co 7421	. 2 class (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
9	4, 8	wceq 1569	1 wff ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)

This definition is used by:  s3eqd  15020  s3cld  15028  s3cli  15037  s3fv0  15048  s3fv1  15049  s3fv2  15050  s3len  15051  s3tpop  15066  s4prop  15067  s3co  15078  s1s2  15080  s1s3  15081  s2s2  15086  s4s3  15088  s3s4  15090  s3eqs2s1eq  15095  repsw3  15110  s3rn  15123  2pthon3v  30538  konigsberglem1  30859  konigsberglem2  30860  konigsberglem3  30861  numtowerdt  48010