Definition df-s2 14814

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 14807	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14560	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14560	. . 3 class ⟨“𝐵”⟩
6		cconcat 14535	. . 3 class ++
7	4, 5, 6	co 7387	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1540	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14828  s2eqd  14829  s2cld  14837  s2cli  14846  s2fv0  14853  s2fv1  14854  s2len  14855  s2prop  14873  s2co  14886  s1s2  14889  s2s2  14895  s4s2  14896  s2s5  14900  s5s2  14901  s2eq2s1eq  14902  swrds2  14906  repsw2  14916  ccatw2s1ccatws2  14920  s2rn  14929  ofs2  14937  gsumws2  18769  efginvrel2  19657  efgredlemc  19675  frgpnabllem1  19803  2pthon3v  29873  konigsberglem1  30181  konigsberglem2  30182  konigsberglem3  30183  cshw1s2  32882  ofcs2  34536