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 14633	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14633	. . 3 class ⟨“𝐵”⟩
6		cconcat 14608	. . 3 class ++
7	4, 5, 6	co 7431	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1540	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  18855  efginvrel2  19745  efgredlemc  19763  frgpnabllem1  19891  2pthon3v  29963  konigsberglem1  30271  konigsberglem2  30272  konigsberglem3  30273  cshw1s2  32945  ofcs2  34560