Metamath Proof Explorer

Theorem s1fv

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

Ref Expression
Assertion s1fv 
|- ( A e. B -> ( <" A "> ` 0 ) = A )

Proof

Step Hyp Ref Expression
1 s1val 
 |-  ( A e. B -> <" A "> = { <. 0 , A >. } )
2 1 fveq1d 
 |-  ( A e. B -> ( <" A "> ` 0 ) = ( { <. 0 , A >. } ` 0 ) )
3 0nn0 
 |-  0 e. NN0
4 fvsng 
 |-  ( ( 0 e. NN0 /\ A e. B ) -> ( { <. 0 , A >. } ` 0 ) = A )
5 3 4 mpan 
 |-  ( A e. B -> ( { <. 0 , A >. } ` 0 ) = A )
6 2 5 eqtrd 
 |-  ( A e. B -> ( <" A "> ` 0 ) = A )