Definition df-s2 12770

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 12763	. 2 class <" A B ">
4	1	cs1 12497	. . 3 class <" A ">
5	2	cs1 12497	. . 3 class <" B ">
6		cconcat 12496	. . 3 class concat
7	4, 5, 6	co 6282	. 2 class ( <" A "> concat <" B "> )
8	3, 7	wceq 1379	1 wff <" A B "> = ( <" A "> concat <" B "> )

This definition is referenced by:  s2eqd  12784  s2cld  12791  s2cli  12800  s2fv0  12807  s2fv1  12808  s2len  12809  s2prop  12819  s2co  12825  s1s2  12828  s2s2  12834  s4s2  12835  s2eq2s1eq  12838  swrds2  12840  repsw2  12845  ccatw2s1ccatws2  12849  gsumws2  15830  efginvrel2  16538  efgredlemc  16556  frgpnabllem1  16665  konigsberg  24660  ofs2  28138  ofcs2  28139