Definition df-s2 14759

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 14752	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14507	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14507	. . 3 class ⟨“𝐵”⟩
6		cconcat 14481	. . 3 class ++
7	4, 5, 6	co 7354	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1541	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14773  s2eqd  14774  s2cld  14782  s2cli  14791  s2fv0  14798  s2fv1  14799  s2len  14800  s2prop  14818  s2co  14831  s1s2  14834  s2s2  14840  s4s2  14841  s2s5  14845  s5s2  14846  s2eq2s1eq  14847  swrds2  14851  repsw2  14861  ccatw2s1ccatws2  14865  s2rn  14874  ofs2  14882  gsumws2  18754  efginvrel2  19643  efgredlemc  19661  frgpnabllem1  19789  2pthon3v  29925  konigsberglem1  30236  konigsberglem2  30237  konigsberglem3  30238  cshw1s2  32950  ofcs2  34581  nthrucw  47011