Definition df-s2 14881

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 14874	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14629	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14629	. . 3 class ⟨“𝐵”⟩
6		cconcat 14603	. . 3 class ++
7	4, 5, 6	co 7408	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1567	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14895  s2eqd  14896  s2cld  14904  s2cli  14913  s2fv0  14920  s2fv1  14921  s2len  14922  s2prop  14940  s2co  14953  s1s2  14956  s2s2  14962  s4s2  14963  s2s5  14967  s5s2  14968  s2eq2s1eq  14969  swrds2  14973  repsw2  14983  ccatw2s1ccatws2  14987  s2rn  14996  ofs2  15004  gsumws2  18897  efginvrel2  19793  efgredlemc  19811  frgpnabllem1  19939  2pthon3v  30229  konigsberglem1  30540  konigsberglem2  30541  konigsberglem3  30542  cshw1s2  33217  ofcs2  34876  nthrucw  47487