Definition df-s2 14796

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

This definition is referenced by:  cats2cat  14810  s2eqd  14811  s2cld  14819  s2cli  14828  s2fv0  14835  s2fv1  14836  s2len  14837  s2prop  14855  s2co  14868  s1s2  14871  s2s2  14877  s4s2  14878  s2s5  14882  s5s2  14883  s2eq2s1eq  14884  swrds2  14888  repsw2  14898  ccatw2s1ccatws2  14902  ofs2  14915  gsumws2  18720  efginvrel2  19590  efgredlemc  19608  frgpnabllem1  19736  2pthon3v  29187  konigsberglem1  29495  konigsberglem2  29496  konigsberglem3  29497  cshw1s2  32112  ofcs2  33545