Definition df-s2 14801

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 14794	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14549	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14549	. . 3 class ⟨“𝐵”⟩
6		cconcat 14523	. . 3 class ++
7	4, 5, 6	co 7360	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1542	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14815  s2eqd  14816  s2cld  14824  s2cli  14833  s2fv0  14840  s2fv1  14841  s2len  14842  s2prop  14860  s2co  14873  s1s2  14876  s2s2  14882  s4s2  14883  s2s5  14887  s5s2  14888  s2eq2s1eq  14889  swrds2  14893  repsw2  14903  ccatw2s1ccatws2  14907  s2rn  14916  ofs2  14924  gsumws2  18801  efginvrel2  19693  efgredlemc  19711  frgpnabllem1  19839  2pthon3v  30026  konigsberglem1  30337  konigsberglem2  30338  konigsberglem3  30339  cshw1s2  33035  ofcs2  34705  nthrucw  47332