Definition df-s2 12724

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 12717	. 2 class <" A B ">
4	1	cs1 12441	. . 3 class <" A ">
5	2	cs1 12441	. . 3 class <" B ">
6		cconcat 12440	. . 3 class ++
7	4, 5, 6	co 6196	. 2 class ( <" A "> ++ <" B "> )
8	3, 7	wceq 1399	1 wff <" A B "> = ( <" A "> ++ <" B "> )

This definition is referenced by:  s2eqd  12738  s2cld  12745  s2cli  12754  s2fv0  12761  s2fv1  12762  s2len  12763  s2prop  12773  s2co  12779  s1s2  12782  s2s2  12788  s4s2  12789  s2eq2s1eq  12792  swrds2  12794  repsw2  12799  ccatw2s1ccatws2  12803  gsumws2  16127  efginvrel2  16862  efgredlemc  16880  frgpnabllem1  16994  konigsberg  25108  ofs2  28684  ofcs2  28685