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	$⊢ ⟨“ A B ”⟩ = ⟨“ A ”⟩ ++ ⟨“ B ”⟩$

Step	Hyp	Ref	Expression
0		cA	$class A$
1		cB	$class B$
2	0 1	cs2	$class ⟨“ A B ”⟩$
3	0	cs1	$class ⟨“ A ”⟩$
4		cconcat	$class ++$
5	1	cs1	$class ⟨“ B ”⟩$
6	3 5 4	co	$class (⟨“ A ”⟩ ++ ⟨“ B ”⟩)$
7	2 6	wceq	$wff ⟨“ A B ”⟩ = ⟨“ A ”⟩ ++ ⟨“ B ”⟩$