Metamath Proof Explorer


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 ) ">