Definition df-s2 12929

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 12922	. 2 class <" A B ">
4	1	cs1 12646	. . 3 class <" A ">
5	2	cs1 12646	. . 3 class <" B ">
6		cconcat 12645	. . 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  12943  s2cld  12950  s2cli  12959  s2fv0  12966  s2fv1  12967  s2len  12968  s2prop  12978  s2co  12984  s1s2  12987  s2s2  12993  s4s2  12994  s2eq2s1eq  12997  swrds2  12999  repsw2  13004  ccatw2s1ccatws2  13008  gsumws2  16577  efginvrel2  17312  efgredlemc  17330  frgpnabllem1  17444  konigsberg  25560  ofs2  29221  ofcs2  29222