Definition df-s2 14783

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 14776	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14531	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14531	. . 3 class ⟨“𝐵”⟩
6		cconcat 14505	. . 3 class ++
7	4, 5, 6	co 7368	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1542	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14797  s2eqd  14798  s2cld  14806  s2cli  14815  s2fv0  14822  s2fv1  14823  s2len  14824  s2prop  14842  s2co  14855  s1s2  14858  s2s2  14864  s4s2  14865  s2s5  14869  s5s2  14870  s2eq2s1eq  14871  swrds2  14875  repsw2  14885  ccatw2s1ccatws2  14889  s2rn  14898  ofs2  14906  gsumws2  18779  efginvrel2  19668  efgredlemc  19686  frgpnabllem1  19814  2pthon3v  30028  konigsberglem1  30339  konigsberglem2  30340  konigsberglem3  30341  cshw1s2  33052  ofcs2  34722  nthrucw  47241