This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-s2

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ⊢ 𝐴
1 cB ⊢ 𝐵
2 0 1 cs2 ⊢ ⟨“ 𝐴 𝐵 ”⟩
3 0 cs1 ⊢ ⟨“ 𝐴 ”⟩
4 cconcat ⊢ ++
5 1 cs1 ⊢ ⟨“ 𝐵 ”⟩
6 3 5 4 co ⊢ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ )
7 2 6 wceq ⊢ ⟨“ 𝐴 𝐵 ”⟩ = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ )