Definition df-s2 12795

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 12788	. 2 class <" A B ">
4	1	cs1 12519	. . 3 class <" A ">
5	2	cs1 12519	. . 3 class <" B ">
6		cconcat 12518	. . 3 class concat
7	4, 5, 6	co 6281	. 2 class ( <" A "> concat <" B "> )
8	3, 7	wceq 1383	1 wff <" A B "> = ( <" A "> concat <" B "> )

This definition is referenced by:  s2eqd  12809  s2cld  12816  s2cli  12825  s2fv0  12832  s2fv1  12833  s2len  12834  s2prop  12844  s2co  12850  s1s2  12853  s2s2  12859  s4s2  12860  s2eq2s1eq  12863  swrds2  12865  repsw2  12870  ccatw2s1ccatws2  12874  gsumws2  15989  efginvrel2  16724  efgredlemc  16742  frgpnabllem1  16856  konigsberg  24965  ofs2  28479  ofcs2  28480