Metamath Proof Explorer

Theorem s1val

Description: Value of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s1val 
|- ( A e. V -> <" A "> = { <. 0 , A >. } )

Proof

Step Hyp Ref Expression
1 df-s1 
 |-  <" A "> = { <. 0 , ( _I ` A ) >. }
2 fvi 
 |-  ( A e. V -> ( _I ` A ) = A )
3 2 opeq2d 
 |-  ( A e. V -> <. 0 , ( _I ` A ) >. = <. 0 , A >. )
4 3 sneqd 
 |-  ( A e. V -> { <. 0 , ( _I ` A ) >. } = { <. 0 , A >. } )
5 1 4 syl5eq 
 |-  ( A e. V -> <" A "> = { <. 0 , A >. } )