Definition df-s2 14046

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 14039	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 13793	. . 3 class ⟨“𝐴”⟩
5	2	cs1 13793	. . 3 class ⟨“𝐵”⟩
6		cconcat 13768	. . 3 class ++
7	4, 5, 6	co 7016	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1522	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14060  s2eqd  14061  s2cld  14069  s2cli  14078  s2fv0  14085  s2fv1  14086  s2len  14087  s2prop  14105  s2co  14118  s1s2  14121  s2s2  14127  s4s2  14128  s2s5  14132  s5s2  14133  s2eq2s1eq  14134  swrds2  14138  repsw2  14148  ccatw2s1ccatws2  14152  ofs2  14165  gsumws2  17818  efginvrel2  18580  efgredlemc  18598  frgpnabllem1  18716  2pthon3v  27409  konigsberglem1  27721  konigsberglem2  27722  konigsberglem3  27723  cshw1s2  30308  ofcs2  31432