Description: Identity function protection for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | ids1 | |- <" A "> = <" ( _I ` A ) "> |
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 ) "> |