Theorem s1eq

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

	Ref	Expression
Assertion	s1eq	⊢ ( 𝐴 = 𝐵 → ⟨“ 𝐴 ”⟩ = ⟨“ 𝐵 ”⟩ )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝐴 = 𝐵 → ( I ‘ 𝐴 ) = ( I ‘ 𝐵 ) )
2	1	opeq2d	⊢ ( 𝐴 = 𝐵 → ⟨ 0 , ( I ‘ 𝐴 ) ⟩ = ⟨ 0 , ( I ‘ 𝐵 ) ⟩ )
3	2	sneqd	⊢ ( 𝐴 = 𝐵 → { ⟨ 0 , ( I ‘ 𝐴 ) ⟩ } = { ⟨ 0 , ( I ‘ 𝐵 ) ⟩ } )
4		df-s1	⊢ ⟨“ 𝐴 ”⟩ = { ⟨ 0 , ( I ‘ 𝐴 ) ⟩ }
5		df-s1	⊢ ⟨“ 𝐵 ”⟩ = { ⟨ 0 , ( I ‘ 𝐵 ) ⟩ }
6	3 4 5	3eqtr4g	⊢ ( 𝐴 = 𝐵 → ⟨“ 𝐴 ”⟩ = ⟨“ 𝐵 ”⟩ )