Definition df-s2 14887

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 14880	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14635	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14635	. . 3 class ⟨“𝐵”⟩
6		cconcat 14609	. . 3 class ++
7	4, 5, 6	co 7412	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1570	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14901  s2eqd  14902  s2cld  14910  s2cli  14919  s2fv0  14926  s2fv1  14927  s2len  14928  s2prop  14946  s2co  14959  s1s2  14962  s2s2  14968  s4s2  14969  s2s5  14973  s5s2  14974  s2eq2s1eq  14975  swrds2  14979  repsw2  14989  ccatw2s1ccatws2  14993  s2rn  15002  ofs2  15010  gsumws2  18902  efginvrel2  19798  efgredlemc  19816  frgpnabllem1  19944  2pthon3v  30273  konigsberglem1  30584  konigsberglem2  30585  konigsberglem3  30586  cshw1s2  33261  ofcs2  34916  nthrucw  47590