Definition df-s2 13593

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 13586	. 2 class <" A B ">
4	1	cs1 13294	. . 3 class <" A ">
5	2	cs1 13294	. . 3 class <" B ">
6		cconcat 13293	. . 3 class ++
7	4, 5, 6	co 6650	. 2 class ( <" A "> ++ <" B "> )
8	3, 7	wceq 1483	1 wff <" A B "> = ( <" A "> ++ <" B "> )

This definition is referenced by:  cats2cat  13607  s2eqd  13608  s2cld  13616  s2cli  13625  s2fv0  13632  s2fv1  13633  s2len  13634  s2prop  13652  s2co  13665  s1s2  13668  s2s2  13674  s4s2  13675  s2s5  13679  s5s2  13680  s2eq2s1eq  13681  swrds2  13685  repsw2  13693  ccatw2s1ccatws2  13697  ofs2  13710  gsumws2  17379  efginvrel2  18140  efgredlemc  18158  frgpnabllem1  18276  2pthon3v  26839  konigsberglem1  27114  konigsberglem2  27115  konigsberglem3  27116  ofcs2  30622