Definition df-s2 14884

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 14877	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14632	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14632	. . 3 class ⟨“𝐵”⟩
6		cconcat 14606	. . 3 class ++
7	4, 5, 6	co 7411	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1567	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14898  s2eqd  14899  s2cld  14907  s2cli  14916  s2fv0  14923  s2fv1  14924  s2len  14925  s2prop  14943  s2co  14956  s1s2  14959  s2s2  14965  s4s2  14966  s2s5  14970  s5s2  14971  s2eq2s1eq  14972  swrds2  14976  repsw2  14986  ccatw2s1ccatws2  14990  s2rn  14999  ofs2  15007  gsumws2  18900  efginvrel2  19796  efgredlemc  19814  frgpnabllem1  19942  2pthon3v  30232  konigsberglem1  30543  konigsberglem2  30544  konigsberglem3  30545  cshw1s2  33220  ofcs2  34879  nthrucw  47493