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

Metamath Proof Explorer

Theorem s1fv

Description: Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

		Ref	Expression
	Assertion	s1fv	$⊢ A \in B \to ⟨“ A ”⟩ (0) = A$

Step	Hyp	Ref	Expression
1		s1val	$⊢ A \in B \to ⟨“ A ”⟩ = \{⟨0, A⟩\}$
2	1	fveq1d	$⊢ A \in B \to ⟨“ A ”⟩ (0) = \{⟨0, A⟩\} (0)$
3		0nn0	$⊢ 0 \in ℕ_{0}$
4		fvsng	$⊢ (0 \in ℕ_{0} \land A \in B) \to \{⟨0, A⟩\} (0) = A$
5	3 4	mpan	$⊢ A \in B \to \{⟨0, A⟩\} (0) = A$
6	2 5	eqtrd	$⊢ A \in B \to ⟨“ A ”⟩ (0) = A$