Definition df-s2 14755

Description: Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)

Assertion

Ref	Expression
df-s2	⊢ ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

Detailed syntax breakdown of Definition df-s2

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cs2 14748	. 2 class ⟨“𝐴𝐵”⟩
4	1	cs1 14503	. . 3 class ⟨“𝐴”⟩
5	2	cs1 14503	. . 3 class ⟨“𝐵”⟩
6		cconcat 14477	. . 3 class ++
7	4, 5, 6	co 7346	. 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
8	3, 7	wceq 1541	1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

This definition is referenced by:  cats2cat  14769  s2eqd  14770  s2cld  14778  s2cli  14787  s2fv0  14794  s2fv1  14795  s2len  14796  s2prop  14814  s2co  14827  s1s2  14830  s2s2  14836  s4s2  14837  s2s5  14841  s5s2  14842  s2eq2s1eq  14843  swrds2  14847  repsw2  14857  ccatw2s1ccatws2  14861  s2rn  14870  ofs2  14878  gsumws2  18750  efginvrel2  19640  efgredlemc  19658  frgpnabllem1  19786  2pthon3v  29922  konigsberglem1  30230  konigsberglem2  30231  konigsberglem3  30232  cshw1s2  32939  ofcs2  34556