Theorem qsexg

Description: A quotient set exists. (Contributed by FL, 19-May-2007) (Revised by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Assertion	qsexg	$$⊢A\in V\to A/R\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-qs	$$⊢A/R=\left\{y|\exists x\in Ay=\left[x\right]R\right\}$$
2		abrexexg	$$⊢A\in V\to \left\{y|\exists x\in Ay=\left[x\right]R\right\}\in \mathrm{V}$$
3	1 2	eqeltrid	$$⊢A\in V\to A/R\in \mathrm{V}$$