Definition df-s2 14755

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

This definition is referenced by:  cats2cat  14769  s2eqd  14770  s2cld  14778  s2cli  14787  s2fv0  14794  s2fv1  14795  s2len  14796  s2prop  14814  s2co  14827  s1s2  14830  s2s2  14836  s4s2  14837  s2s5  14841  s5s2  14842  s2eq2s1eq  14843  swrds2  14847  repsw2  14857  ccatw2s1ccatws2  14861  s2rn  14870  ofs2  14878  gsumws2  18716  efginvrel2  19606  efgredlemc  19624  frgpnabllem1  19752  2pthon3v  29892  konigsberglem1  30200  konigsberglem2  30201  konigsberglem3  30202  cshw1s2  32911  ofcs2  34529