Definition df-s2 14919

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

This definition is used by:  cats2cat  14933  s2eqd  14934  s2cld  14942  s2cli  14951  s2fv0  14958  s2fv1  14959  s2len  14960  s2prop  14978  s2co  14991  s1s2  14994  s2s2  15000  s4s2  15001  s2s5  15005  s5s2  15006  s2eq2s1eq  15007  swrds2  15011  repsw2  15023  ccatw2s1ccatws2  15027  s2rn  15036  ofs2  15044  gsumws2  18951  efginvrel2  19854  efgredlemc  19872  frgpnabllem1  20000  2pthon3v  30411  konigsberglem1  30732  konigsberglem2  30733  konigsberglem3  30734  cshw1s2  33400  ofcs2  35056  numtowerdt  47734