Definition df-s2 14808

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 14801	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14556	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14556	. . 3 class ⟨“𝐵”⟩
6		cconcat 14530	. . 3 class ++
7	4, 5, 6	co 7363	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1547	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14822  s2eqd  14823  s2cld  14831  s2cli  14840  s2fv0  14847  s2fv1  14848  s2len  14849  s2prop  14867  s2co  14880  s1s2  14883  s2s2  14889  s4s2  14890  s2s5  14894  s5s2  14895  s2eq2s1eq  14896  swrds2  14900  repsw2  14910  ccatw2s1ccatws2  14914  s2rn  14923  ofs2  14931  gsumws2  18808  efginvrel2  19700  efgredlemc  19718  frgpnabllem1  19846  2pthon3v  30036  konigsberglem1  30347  konigsberglem2  30348  konigsberglem3  30349  cshw1s2  33046  ofcs2  34736  nthrucw  47338