Definition df-s4 13392

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 13385	. 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
6	1, 2, 3	cs3 13384	. . 3 class ⟨“𝐴𝐵𝐶”⟩
7	4	cs1 13095	. . 3 class ⟨“𝐷”⟩
8		cconcat 13094	. . 3 class ++
9	6, 7, 8	co 6527	. 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
10	5, 9	wceq 1474	1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)

This definition is referenced by:  s4eqd  13407  s4cld  13414  s4cli  13423  s4fv0  13436  s4fv1  13437  s4fv2  13438  s4fv3  13439  s4len  13440  s4prop  13451  s1s3  13465  s1s4  13466  s2s2  13470  s4s4  13473  tgcgr4  25144  usgraexmplvtx  25697  konigsberg  26280  konigsberglem1  41417  konigsberglem2  41418  konigsberglem3  41419