Definition df-s2 13444

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 13437	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 13149	. . 3 class ⟨“𝐴”⟩
5	2	cs1 13149	. . 3 class ⟨“𝐵”⟩
6		cconcat 13148	. . 3 class ++
7	4, 5, 6	co 6549	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1475	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  13458  s2eqd  13459  s2cld  13466  s2cli  13475  s2fv0  13482  s2fv1  13483  s2len  13484  s2prop  13502  s2co  13515  s1s2  13518  s2s2  13524  s4s2  13525  s2s5  13529  s5s2  13530  s2eq2s1eq  13531  swrds2  13533  repsw2  13541  ccatw2s1ccatws2  13545  ofs2  13558  gsumws2  17202  efginvrel2  17963  efgredlemc  17981  frgpnabllem1  18099  konigsberg  26514  ofcs2  29948  2pthon3v-av  41150  konigsberglem1  41422  konigsberglem2  41423  konigsberglem3  41424