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”⟩\left(0\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		s1val	$$⊢A\in B\to ⟨“A”⟩=\left\{⟨0,A⟩\right\}$$
2	1	fveq1d	$$⊢A\in B\to ⟨“A”⟩\left(0\right)=\left\{⟨0,A⟩\right\}\left(0\right)$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4		fvsng	$$⊢\left(0\in {\mathbb{N}}_0\wedge A\in B\right)\to \left\{⟨0,A⟩\right\}\left(0\right)=A$$
5	3 4	mpan	$$⊢A\in B\to \left\{⟨0,A⟩\right\}\left(0\right)=A$$
6	2 5	eqtrd	$$⊢A\in B\to ⟨“A”⟩\left(0\right)=A$$