Definition df-s2 12946

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 12939	. 2 class <" A B ">
4	1	cs1 12663	. . 3 class <" A ">
5	2	cs1 12663	. . 3 class <" B ">
6		cconcat 12662	. . 3 class ++
7	4, 5, 6	co 6305	. 2 class ( <" A "> ++ <" B "> )
8	3, 7	wceq 1437	1 wff <" A B "> = ( <" A "> ++ <" B "> )

This definition is referenced by:  s2eqd  12960  s2cld  12967  s2cli  12976  s2fv0  12983  s2fv1  12984  s2len  12985  s2prop  12999  s2co  13005  s1s2  13008  s2s2  13014  s4s2  13015  s2eq2s1eq  13018  swrds2  13020  repsw2  13025  ccatw2s1ccatws2  13029  gsumws2  16625  efginvrel2  17376  efgredlemc  17394  frgpnabllem1  17508  konigsberg  25713  ofs2  29441  ofcs2  29442