Definition df-s2 12594

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 12587	. 2 class <" A B ">
4	1	cs1 12343	. . 3 class <" A ">
5	2	cs1 12343	. . 3 class <" B ">
6		cconcat 12342	. . 3 class concat
7	4, 5, 6	co 6201	. 2 class ( <" A "> concat <" B "> )
8	3, 7	wceq 1370	1 wff <" A B "> = ( <" A "> concat <" B "> )

This definition is referenced by:  s2eqd  12608  s2cld  12615  s2cli  12624  s2fv0  12631  s2fv1  12632  s2len  12633  s2prop  12643  s2co  12649  s1s2  12652  s2s2  12658  s4s2  12659  s2eq2s1eq  12662  swrds2  12664  repsw2  12669  ccatw2s1ccatws2  12673  gsumws2  15640  efginvrel2  16346  efgredlemc  16364  frgpnabllem1  16473  konigsberg  23761  ofs2  27090  ofcs2  27091