wrdlen2s2

Description: A word of length two as doubleton word. (Contributed by AV, 20-Oct-2018)

		Ref	Expression
	Assertion	wrdlen2s2	$⊢ (W \in Word V \land \|W\| = 2) \to W = ⟨“ W (0) W (1) ”⟩$

Step	Hyp	Ref	Expression
1		wrd2pr2op	$⊢ (W \in Word V \land \|W\| = 2) \to W = \{⟨0, W (0)⟩, ⟨1, W (1)⟩\}$
2		fvex	$⊢ W (0) \in V$
3		fvex	$⊢ W (1) \in V$
4		s2prop	$⊢ (W (0) \in V \land W (1) \in V) \to ⟨“ W (0) W (1) ”⟩ = \{⟨0, W (0)⟩, ⟨1, W (1)⟩\}$
5	4	eqcomd	$⊢ (W (0) \in V \land W (1) \in V) \to \{⟨0, W (0)⟩, ⟨1, W (1)⟩\} = ⟨“ W (0) W (1) ”⟩$
6	2 3 5	mp2an	$⊢ \{⟨0, W (0)⟩, ⟨1, W (1)⟩\} = ⟨“ W (0) W (1) ”⟩$
7	1 6	eqtrdi	$⊢ (W \in Word V \land \|W\| = 2) \to W = ⟨“ W (0) W (1) ”⟩$

Metamath Proof Explorer