Definition df-s2 14799

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

This definition is referenced by:  cats2cat  14813  s2eqd  14814  s2cld  14822  s2cli  14831  s2fv0  14838  s2fv1  14839  s2len  14840  s2prop  14858  s2co  14871  s1s2  14874  s2s2  14880  s4s2  14881  s2s5  14885  s5s2  14886  s2eq2s1eq  14887  swrds2  14891  repsw2  14901  ccatw2s1ccatws2  14905  ofs2  14918  gsumws2  18723  efginvrel2  19595  efgredlemc  19613  frgpnabllem1  19741  2pthon3v  29197  konigsberglem1  29505  konigsberglem2  29506  konigsberglem3  29507  cshw1s2  32124  ofcs2  33556