Theorem ids1

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

	Ref	Expression
Assertion	ids1	|- <" A "> = <" ( _I ` A ) ">

Proof

Step	Hyp	Ref	Expression
1		fvex	|- ( _I ` A ) e. _V
2		fvi	|- ( ( _I ` A ) e. _V -> ( _I ` ( _I ` A ) ) = ( _I ` A ) )
3	1 2	ax-mp	|- ( _I ` ( _I ` A ) ) = ( _I ` A )
4	3	opeq2i	|- <. 0 , ( _I ` ( _I ` A ) ) >. = <. 0 , ( _I ` A ) >.
5	4	sneqi	|- { <. 0 , ( _I ` ( _I ` A ) ) >. } = { <. 0 , ( _I ` A ) >. }
6		df-s1	|- <" ( _I ` A ) "> = { <. 0 , ( _I ` ( _I ` A ) ) >. }
7		df-s1	|- <" A "> = { <. 0 , ( _I ` A ) >. }
8	5 6 7	3eqtr4ri	|- <" A "> = <" ( _I ` A ) ">