Definition df-s2 14821

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

This definition is referenced by:  cats2cat  14835  s2eqd  14836  s2cld  14844  s2cli  14853  s2fv0  14860  s2fv1  14861  s2len  14862  s2prop  14880  s2co  14893  s1s2  14896  s2s2  14902  s4s2  14903  s2s5  14907  s5s2  14908  s2eq2s1eq  14909  swrds2  14913  repsw2  14923  ccatw2s1ccatws2  14927  s2rn  14936  ofs2  14944  gsumws2  18776  efginvrel2  19664  efgredlemc  19682  frgpnabllem1  19810  2pthon3v  29880  konigsberglem1  30188  konigsberglem2  30189  konigsberglem3  30190  cshw1s2  32889  ofcs2  34543