Definition df-s2 11767

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 11760	. 2 class <" A B ">
4	1	cs1 11674	. . 3 class <" A ">
5	2	cs1 11674	. . 3 class <" B ">
6		cconcat 11673	. . 3 class concat
7	4, 5, 6	co 6040	. 2 class ( <" A "> concat <" B "> )
8	3, 7	wceq 1649	1 wff <" A B "> = ( <" A "> concat <" B "> )

This definition is referenced by:  s2eqd  11781  s2cld  11788  s2cli  11797  s2fv0  11804  s2fv1  11805  s2len  11806  s2prop  11816  s2co  11822  s1s2  11825  s2s2  11831  s4s2  11832  swrds2  11835  gsumws2  14743  efginvrel2  15314  efgredlemc  15332  frgpnabllem1  15439  konigsberg  21662