Definition df-s2 14210

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

Assertion

Ref	Expression
df-s2	⊢ ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

Detailed syntax breakdown of Definition df-s2

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cs2 14203	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 13949	. . 3 class ⟨“𝐴”⟩
5	2	cs1 13949	. . 3 class ⟨“𝐵”⟩
6		cconcat 13922	. . 3 class ++
7	4, 5, 6	co 7156	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1537	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14224  s2eqd  14225  s2cld  14233  s2cli  14242  s2fv0  14249  s2fv1  14250  s2len  14251  s2prop  14269  s2co  14282  s1s2  14285  s2s2  14291  s4s2  14292  s2s5  14296  s5s2  14297  s2eq2s1eq  14298  swrds2  14302  repsw2  14312  ccatw2s1ccatws2  14316  ccatw2s1ccatws2OLD  14317  ofs2  14331  gsumws2  18007  efginvrel2  18853  efgredlemc  18871  frgpnabllem1  18993  2pthon3v  27722  konigsberglem1  28031  konigsberglem2  28032  konigsberglem3  28033  cshw1s2  30634  ofcs2  31815