Theorem ids1

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

	Ref	Expression
Assertion	ids1	$$⊢⟨“A”⟩=⟨“\mathrm{I}\left(A\right)”⟩$$

Proof

Step	Hyp	Ref	Expression
1		fvex	$$⊢\mathrm{I}\left(A\right)\in \mathrm{V}$$
2		fvi	$$⊢\mathrm{I}\left(A\right)\in \mathrm{V}\to \mathrm{I}\left(\mathrm{I}\left(A\right)\right)=\mathrm{I}\left(A\right)$$
3	1 2	ax-mp	$$⊢\mathrm{I}\left(\mathrm{I}\left(A\right)\right)=\mathrm{I}\left(A\right)$$
4	3	opeq2i	$$⊢⟨0,\mathrm{I}\left(\mathrm{I}\left(A\right)\right)⟩=⟨0,\mathrm{I}\left(A\right)⟩$$
5	4	sneqi	$$⊢\left\{⟨0,\mathrm{I}\left(\mathrm{I}\left(A\right)\right)⟩\right\}=\left\{⟨0,\mathrm{I}\left(A\right)⟩\right\}$$
6		df-s1	$$⊢⟨“\mathrm{I}\left(A\right)”⟩=\left\{⟨0,\mathrm{I}\left(\mathrm{I}\left(A\right)\right)⟩\right\}$$
7		df-s1	$$⊢⟨“A”⟩=\left\{⟨0,\mathrm{I}\left(A\right)⟩\right\}$$
8	5 6 7	3eqtr4ri	$$⊢⟨“A”⟩=⟨“\mathrm{I}\left(A\right)”⟩$$