Metamath Proof Explorer

Theorem eceq2

Description: Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995)

Ref Expression
Assertion eceq2 
|- ( A = B -> [ C ] A = [ C ] B )

Proof

Step Hyp Ref Expression
1 imaeq1 
 |-  ( A = B -> ( A " { C } ) = ( B " { C } ) )
2 df-ec 
 |-  [ C ] A = ( A " { C } )
3 df-ec 
 |-  [ C ] B = ( B " { C } )
4 1 2 3 3eqtr4g 
 |-  ( A = B -> [ C ] A = [ C ] B )