Definition df-s2 15041

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

This definition is used by:  cats2cat  15055  s2eqd  15056  s2cld  15064  s2cli  15073  s2fv0  15080  s2fv1  15081  s2len  15082  s2prop  15101  s2co  15114  s1s2  15117  s2s2  15123  s4s2  15124  s2s5  15128  s5s2  15129  s2eq2s1eq  15130  swrds2  15134  repsw2  15146  ccatw2s1ccatws2  15150  s2rn  15159  ofs2  15167  gsumws2  19088  efginvrel2  19992  efgredlemc  20010  frgpnabllem1  20138  2pthon3v  30589  konigsberglem1  30910  konigsberglem2  30911  konigsberglem3  30912  cshw1s2  33617  ofcs2  35288  numtowerdt  48189