Definition df-s2 14854

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 14847	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14602	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14602	. . 3 class ⟨“𝐵”⟩
6		cconcat 14576	. . 3 class ++
7	4, 5, 6	co 7390	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1559	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14868  s2eqd  14869  s2cld  14877  s2cli  14886  s2fv0  14893  s2fv1  14894  s2len  14895  s2prop  14913  s2co  14926  s1s2  14929  s2s2  14935  s4s2  14936  s2s5  14940  s5s2  14941  s2eq2s1eq  14942  swrds2  14946  repsw2  14956  ccatw2s1ccatws2  14960  s2rn  14969  ofs2  14977  gsumws2  18866  efginvrel2  19757  efgredlemc  19775  frgpnabllem1  19903  2pthon3v  30099  konigsberglem1  30410  konigsberglem2  30411  konigsberglem3  30412  cshw1s2  33098  ofcs2  34802  nthrucw  47422