Theorem ecexg

Description: An equivalence class modulo a set is a set. (Contributed by NM, 24-Jul-1995)

	Ref	Expression
Assertion	ecexg	$$⊢R\in B\to \left[A\right]R\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-ec	$$⊢\left[A\right]R=R\left[\left\{A\right\}\right]$$
2		imaexg	$$⊢R\in B\to R\left[\left\{A\right\}\right]\in \mathrm{V}$$
3	1 2	eqeltrid	$$⊢R\in B\to \left[A\right]R\in \mathrm{V}$$