Definition df-s2 15004

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 14997	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14746	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14746	. . 3 class ⟨“𝐵”⟩
6		cconcat 14719	. . 3 class ++
7	4, 5, 6	co 7421	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1569	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is used by:  cats2cat  15018  s2eqd  15019  s2cld  15027  s2cli  15036  s2fv0  15043  s2fv1  15044  s2len  15045  s2prop  15064  s2co  15077  s1s2  15080  s2s2  15086  s4s2  15087  s2s5  15091  s5s2  15092  s2eq2s1eq  15093  swrds2  15097  repsw2  15109  ccatw2s1ccatws2  15113  s2rn  15122  ofs2  15130  gsumws2  19044  efginvrel2  19947  efgredlemc  19965  frgpnabllem1  20093  2pthon3v  30538  konigsberglem1  30859  konigsberglem2  30860  konigsberglem3  30861  cshw1s2  33568  ofcs2  35224  numtowerdt  48010