Definition df-s2 12467

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

Assertion

Ref	Expression
df-s2	|- <" A B "> = ( <" A "> concat <" 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 12460	. 2 class <" A B ">
4	1	cs1 12216	. . 3 class <" A ">
5	2	cs1 12216	. . 3 class <" B ">
6		cconcat 12215	. . 3 class concat
7	4, 5, 6	co 6086	. 2 class ( <" A "> concat <" B "> )
8	3, 7	wceq 1369	1 wff <" A B "> = ( <" A "> concat <" B "> )

This definition is referenced by:  s2eqd  12481  s2cld  12488  s2cli  12497  s2fv0  12504  s2fv1  12505  s2len  12506  s2prop  12516  s2co  12522  s1s2  12525  s2s2  12531  s4s2  12532  s2eq2s1eq  12535  swrds2  12537  repsw2  12542  ccatw2s1ccatws2  12546  gsumws2  15511  efginvrel2  16215  efgredlemc  16233  frgpnabllem1  16342  konigsberg  23559  ofs2  26897  ofcs2  26898