Definition df-s2 14378

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 14371	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14117	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14117	. . 3 class ⟨“𝐵”⟩
6		cconcat 14090	. . 3 class ++
7	4, 5, 6	co 7191	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1543	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14392  s2eqd  14393  s2cld  14401  s2cli  14410  s2fv0  14417  s2fv1  14418  s2len  14419  s2prop  14437  s2co  14450  s1s2  14453  s2s2  14459  s4s2  14460  s2s5  14464  s5s2  14465  s2eq2s1eq  14466  swrds2  14470  repsw2  14480  ccatw2s1ccatws2  14484  ccatw2s1ccatws2OLD  14485  ofs2  14499  gsumws2  18223  efginvrel2  19071  efgredlemc  19089  frgpnabllem1  19212  2pthon3v  27981  konigsberglem1  28289  konigsberglem2  28290  konigsberglem3  28291  cshw1s2  30906  ofcs2  32190