Metamath Proof Explorer

Theorem eceq1

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

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

Proof

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