Definition df-s4 13446

Description: Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)

Assertion

Ref	Expression
df-s4	⊢ ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

Detailed syntax breakdown of Definition df-s4

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cC	. . 3 class 𝐶
4		cD	. . 3 class 𝐷
5	1, 2, 3, 4	cs4 13439	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 13438	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 13149	. . 3 class ⟨“𝐷”⟩
8		cconcat 13148	. . 3 class ++
9	6, 7, 8	co 6549	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1475	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  13461  s4cld  13468  s4cli  13477  s4fv0  13490  s4fv1  13491  s4fv2  13492  s4fv3  13493  s4len  13494  s4prop  13505  s1s3  13519  s1s4  13520  s2s2  13524  s4s4  13527  tgcgr4  25226  usgraexmplvtx  25931  konigsberg  26514  konigsberglem1  41422  konigsberglem2  41423  konigsberglem3  41424