Theorem s1val

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

	Ref	Expression
Assertion	s1val	$$⊢A\in V\to ⟨“A”⟩=\left\{⟨0,A⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-s1	$$⊢⟨“A”⟩=\left\{⟨0,\mathrm{I}\left(A\right)⟩\right\}$$
2		fvi	$$⊢A\in V\to \mathrm{I}\left(A\right)=A$$
3	2	opeq2d	$$⊢A\in V\to ⟨0,\mathrm{I}\left(A\right)⟩=⟨0,A⟩$$
4	3	sneqd	$$⊢A\in V\to \left\{⟨0,\mathrm{I}\left(A\right)⟩\right\}=\left\{⟨0,A⟩\right\}$$
5	1 4	eqtrid	$$⊢A\in V\to ⟨“A”⟩=\left\{⟨0,A⟩\right\}$$