Definition df-s2 14904

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 14897	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14647	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14647	. . 3 class ⟨“𝐵”⟩
6		cconcat 14620	. . 3 class ++
7	4, 5, 6	co 7416	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1570	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is used by:  cats2cat  14918  s2eqd  14919  s2cld  14927  s2cli  14936  s2fv0  14943  s2fv1  14944  s2len  14945  s2prop  14963  s2co  14976  s1s2  14979  s2s2  14985  s4s2  14986  s2s5  14990  s5s2  14991  s2eq2s1eq  14992  swrds2  14996  repsw2  15006  ccatw2s1ccatws2  15010  s2rn  15019  ofs2  15027  gsumws2  18924  efginvrel2  19820  efgredlemc  19838  frgpnabllem1  19966  2pthon3v  30321  konigsberglem1  30632  konigsberglem2  30633  konigsberglem3  30634  cshw1s2  33303  ofcs2  34959  nthrucw  47640