Definition df-s2 14489

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 14482	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14228	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14228	. . 3 class ⟨“𝐵”⟩
6		cconcat 14201	. . 3 class ++
7	4, 5, 6	co 7255	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1539	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14503  s2eqd  14504  s2cld  14512  s2cli  14521  s2fv0  14528  s2fv1  14529  s2len  14530  s2prop  14548  s2co  14561  s1s2  14564  s2s2  14570  s4s2  14571  s2s5  14575  s5s2  14576  s2eq2s1eq  14577  swrds2  14581  repsw2  14591  ccatw2s1ccatws2  14595  ccatw2s1ccatws2OLD  14596  ofs2  14610  gsumws2  18396  efginvrel2  19248  efgredlemc  19266  frgpnabllem1  19389  2pthon3v  28209  konigsberglem1  28517  konigsberglem2  28518  konigsberglem3  28519  cshw1s2  31134  ofcs2  32424