Theorem s1eq

Description: Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Assertion	s1eq	$$⊢A=B\to ⟨“A”⟩=⟨“B”⟩$$

Proof

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