Theorem ids1

Description: Identity function protection for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Assertion	ids1	⊢ ⟨“ 𝐴 ”⟩ = ⟨“ ( I ‘ 𝐴 ) ”⟩

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( I ‘ 𝐴 ) ∈ V
2		fvi	⊢ ( ( I ‘ 𝐴 ) ∈ V → ( I ‘ ( I ‘ 𝐴 ) ) = ( I ‘ 𝐴 ) )
3	1 2	ax-mp	⊢ ( I ‘ ( I ‘ 𝐴 ) ) = ( I ‘ 𝐴 )
4	3	opeq2i	⊢ ⟨ 0 , ( I ‘ ( I ‘ 𝐴 ) ) ⟩ = ⟨ 0 , ( I ‘ 𝐴 ) ⟩
5	4	sneqi	⊢ { ⟨ 0 , ( I ‘ ( I ‘ 𝐴 ) ) ⟩ } = { ⟨ 0 , ( I ‘ 𝐴 ) ⟩ }
6		df-s1	⊢ ⟨“ ( I ‘ 𝐴 ) ”⟩ = { ⟨ 0 , ( I ‘ ( I ‘ 𝐴 ) ) ⟩ }
7		df-s1	⊢ ⟨“ 𝐴 ”⟩ = { ⟨ 0 , ( I ‘ 𝐴 ) ⟩ }
8	5 6 7	3eqtr4ri	⊢ ⟨“ 𝐴 ”⟩ = ⟨“ ( I ‘ 𝐴 ) ”⟩