Definition df-s2 14883

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 14876	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14629	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14629	. . 3 class ⟨“𝐵”⟩
6		cconcat 14604	. . 3 class ++
7	4, 5, 6	co 7430	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1536	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14897  s2eqd  14898  s2cld  14906  s2cli  14915  s2fv0  14922  s2fv1  14923  s2len  14924  s2prop  14942  s2co  14955  s1s2  14958  s2s2  14964  s4s2  14965  s2s5  14969  s5s2  14970  s2eq2s1eq  14971  swrds2  14975  repsw2  14985  ccatw2s1ccatws2  14989  s2rn  14998  ofs2  15006  gsumws2  18867  efginvrel2  19759  efgredlemc  19777  frgpnabllem1  19905  2pthon3v  29972  konigsberglem1  30280  konigsberglem2  30281  konigsberglem3  30282  cshw1s2  32929  ofcs2  34538