Definition df-s2 14865

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

This definition is referenced by:  cats2cat  14879  s2eqd  14880  s2cld  14888  s2cli  14897  s2fv0  14904  s2fv1  14905  s2len  14906  s2prop  14924  s2co  14937  s1s2  14940  s2s2  14946  s4s2  14947  s2s5  14951  s5s2  14952  s2eq2s1eq  14953  swrds2  14957  repsw2  14967  ccatw2s1ccatws2  14971  s2rn  14980  ofs2  14988  gsumws2  18818  efginvrel2  19706  efgredlemc  19724  frgpnabllem1  19852  2pthon3v  29871  konigsberglem1  30179  konigsberglem2  30180  konigsberglem3  30181  cshw1s2  32882  ofcs2  34523