Definition df-s2 12459

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 12452	. 2 class <" A B ">
4	1	cs1 12208	. . 3 class <" A ">
5	2	cs1 12208	. . 3 class <" B ">
6		cconcat 12207	. . 3 class concat
7	4, 5, 6	co 6080	. 2 class ( <" A "> concat <" B "> )
8	3, 7	wceq 1362	1 wff <" A B "> = ( <" A "> concat <" B "> )

This definition is referenced by:  s2eqd  12473  s2cld  12480  s2cli  12489  s2fv0  12496  s2fv1  12497  s2len  12498  s2prop  12508  s2co  12514  s1s2  12517  s2s2  12523  s4s2  12524  s2eq2s1eq  12527  swrds2  12529  repsw2  12534  ccatw2s1ccatws2  12538  gsumws2  15500  efginvrel2  16204  efgredlemc  16222  frgpnabllem1  16331  konigsberg  23431  ofs2  26793  ofcs2  26794