Definition df-s2 14810

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 14803	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14558	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14558	. . 3 class ⟨“𝐵”⟩
6		cconcat 14532	. . 3 class ++
7	4, 5, 6	co 7367	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1542	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14824  s2eqd  14825  s2cld  14833  s2cli  14842  s2fv0  14849  s2fv1  14850  s2len  14851  s2prop  14869  s2co  14882  s1s2  14885  s2s2  14891  s4s2  14892  s2s5  14896  s5s2  14897  s2eq2s1eq  14898  swrds2  14902  repsw2  14912  ccatw2s1ccatws2  14916  s2rn  14925  ofs2  14933  gsumws2  18810  efginvrel2  19702  efgredlemc  19720  frgpnabllem1  19848  2pthon3v  30011  konigsberglem1  30322  konigsberglem2  30323  konigsberglem3  30324  cshw1s2  33020  ofcs2  34689  nthrucw  47316