Definition df-s2 14992

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

This definition is used by:  cats2cat  15006  s2eqd  15007  s2cld  15015  s2cli  15024  s2fv0  15031  s2fv1  15032  s2len  15033  s2prop  15051  s2co  15064  s1s2  15067  s2s2  15073  s4s2  15074  s2s5  15078  s5s2  15079  s2eq2s1eq  15080  swrds2  15084  repsw2  15096  ccatw2s1ccatws2  15100  s2rn  15109  ofs2  15117  gsumws2  19031  efginvrel2  19934  efgredlemc  19952  frgpnabllem1  20080  2pthon3v  30525  konigsberglem1  30846  konigsberglem2  30847  konigsberglem3  30848  cshw1s2  33514  ofcs2  35170  numtowerdt  47885