Theorem s1eq

Description: Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Assertion	s1eq	|- ( A = B -> <" A "> = <" B "> )

Proof

Step	Hyp	Ref	Expression
1		fveq2	|- ( A = B -> ( _I ` A ) = ( _I ` B ) )
2	1	opeq2d	|- ( A = B -> <. 0 , ( _I ` A ) >. = <. 0 , ( _I ` B ) >. )
3	2	sneqd	|- ( A = B -> { <. 0 , ( _I ` A ) >. } = { <. 0 , ( _I ` B ) >. } )
4		df-s1	|- <" A "> = { <. 0 , ( _I ` A ) >. }
5		df-s1	|- <" B "> = { <. 0 , ( _I ` B ) >. }
6	3 4 5	3eqtr4g	|- ( A = B -> <" A "> = <" B "> )