Definition df-s2 14786

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 14779	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14532	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14532	. . 3 class ⟨“𝐵”⟩
6		cconcat 14507	. . 3 class ++
7	4, 5, 6	co 7396	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1542	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14800  s2eqd  14801  s2cld  14809  s2cli  14818  s2fv0  14825  s2fv1  14826  s2len  14827  s2prop  14845  s2co  14858  s1s2  14861  s2s2  14867  s4s2  14868  s2s5  14872  s5s2  14873  s2eq2s1eq  14874  swrds2  14878  repsw2  14888  ccatw2s1ccatws2  14892  ofs2  14905  gsumws2  18710  efginvrel2  19579  efgredlemc  19597  frgpnabllem1  19724  2pthon3v  29164  konigsberglem1  29472  konigsberglem2  29473  konigsberglem3  29474  cshw1s2  32095  ofcs2  33487