Theorem ecqs

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

	Ref	Expression
Hypothesis	ecqs.1	$$⊢R\in \mathrm{V}$$
Assertion	ecqs	$$⊢\left[A\right]R=\bigcup \left(\left\{A\right\}/R\right)$$

Proof

Step	Hyp	Ref	Expression
1		ecqs.1	$$⊢R\in \mathrm{V}$$
2		df-ec	$$⊢\left[A\right]R=R\left[\left\{A\right\}\right]$$
3		uniqsw	$$⊢R\in \mathrm{V}\to \bigcup \left(\left\{A\right\}/R\right)=R\left[\left\{A\right\}\right]$$
4	1 3	ax-mp	$$⊢\bigcup \left(\left\{A\right\}/R\right)=R\left[\left\{A\right\}\right]$$
5	2 4	eqtr4i	$$⊢\left[A\right]R=\bigcup \left(\left\{A\right\}/R\right)$$