Description: Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995)
Ref | Expression | ||
---|---|---|---|
Assertion | eceq1 | |- ( A = B -> [ A ] C = [ B ] C ) |
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 ) |