Definition df-s2 14771

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 14764	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14519	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14519	. . 3 class ⟨“𝐵”⟩
6		cconcat 14493	. . 3 class ++
7	4, 5, 6	co 7358	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1541	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14785  s2eqd  14786  s2cld  14794  s2cli  14803  s2fv0  14810  s2fv1  14811  s2len  14812  s2prop  14830  s2co  14843  s1s2  14846  s2s2  14852  s4s2  14853  s2s5  14857  s5s2  14858  s2eq2s1eq  14859  swrds2  14863  repsw2  14873  ccatw2s1ccatws2  14877  s2rn  14886  ofs2  14894  gsumws2  18767  efginvrel2  19656  efgredlemc  19674  frgpnabllem1  19802  2pthon3v  30016  konigsberglem1  30327  konigsberglem2  30328  konigsberglem3  30329  cshw1s2  33042  ofcs2  34702  nthrucw  47130