Definition df-s2 14570

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

This definition is referenced by:  cats2cat  14584  s2eqd  14585  s2cld  14593  s2cli  14602  s2fv0  14609  s2fv1  14610  s2len  14611  s2prop  14629  s2co  14642  s1s2  14645  s2s2  14651  s4s2  14652  s2s5  14656  s5s2  14657  s2eq2s1eq  14658  swrds2  14662  repsw2  14672  ccatw2s1ccatws2  14676  ccatw2s1ccatws2OLD  14677  ofs2  14691  gsumws2  18490  efginvrel2  19342  efgredlemc  19360  frgpnabllem1  19483  2pthon3v  28317  konigsberglem1  28625  konigsberglem2  28626  konigsberglem3  28627  cshw1s2  31241  ofcs2  32533