Definition df-s2 14773

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

This definition is referenced by:  cats2cat  14787  s2eqd  14788  s2cld  14796  s2cli  14805  s2fv0  14812  s2fv1  14813  s2len  14814  s2prop  14832  s2co  14845  s1s2  14848  s2s2  14854  s4s2  14855  s2s5  14859  s5s2  14860  s2eq2s1eq  14861  swrds2  14865  repsw2  14875  ccatw2s1ccatws2  14879  s2rn  14888  ofs2  14896  gsumws2  18734  efginvrel2  19624  efgredlemc  19642  frgpnabllem1  19770  2pthon3v  29906  konigsberglem1  30214  konigsberglem2  30215  konigsberglem3  30216  cshw1s2  32915  ofcs2  34515