Definition df-s2 14897

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 14890	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14643	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14643	. . 3 class ⟨“𝐵”⟩
6		cconcat 14618	. . 3 class ++
7	4, 5, 6	co 7448	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1537	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14911  s2eqd  14912  s2cld  14920  s2cli  14929  s2fv0  14936  s2fv1  14937  s2len  14938  s2prop  14956  s2co  14969  s1s2  14972  s2s2  14978  s4s2  14979  s2s5  14983  s5s2  14984  s2eq2s1eq  14985  swrds2  14989  repsw2  14999  ccatw2s1ccatws2  15003  s2rn  15012  ofs2  15020  gsumws2  18877  efginvrel2  19769  efgredlemc  19787  frgpnabllem1  19915  2pthon3v  29976  konigsberglem1  30284  konigsberglem2  30285  konigsberglem3  30286  cshw1s2  32927  ofcs2  34522