Description: Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ecqs.1 | |
|
Assertion | ecqs | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ecqs.1 | |
|
2 | df-ec | |
|
3 | uniqs | |
|
4 | 1 3 | ax-mp | |
5 | 2 4 | eqtr4i | |