Definition df-s2 12987

Description: Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)

Assertion

Ref	Expression
df-s2	|- <" A B "> = ( <" A "> ++ <" B "> )

Detailed syntax breakdown of Definition df-s2

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cs2 12980	. 2 class <" A B ">
4	1	cs1 12698	. . 3 class <" A ">
5	2	cs1 12698	. . 3 class <" B ">
6		cconcat 12697	. . 3 class ++
7	4, 5, 6	co 6320	. 2 class ( <" A "> ++ <" B "> )
8	3, 7	wceq 1455	1 wff <" A B "> = ( <" A "> ++ <" B "> )

This definition is referenced by:  s2eqd  13001  s2cld  13008  s2cli  13017  s2fv0  13024  s2fv1  13025  s2len  13026  s2prop  13044  s2co  13057  s1s2  13060  s2s2  13066  s4s2  13067  s2eq2s1eq  13070  swrds2  13072  repsw2  13080  ccatw2s1ccatws2  13084  gsumws2  16681  efginvrel2  17432  efgredlemc  17450  frgpnabllem1  17564  konigsberg  25771  ofs2  29483  ofcs2  29484  2pthon3v-av  39988