Metamath Proof Explorer


Theorem ecqs

Description: Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999)

Ref Expression
Hypothesis ecqs.1 RV
Assertion ecqs AR=A/R

Proof

Step Hyp Ref Expression
1 ecqs.1 RV
2 df-ec AR=RA
3 uniqs RVA/R=RA
4 1 3 ax-mp A/R=RA
5 2 4 eqtr4i AR=A/R