Theorem elqsg

Description: Closed form of elqs . (Contributed by Rodolfo Medina, 12-Oct-2010)

	Ref	Expression
Assertion	elqsg	$$⊢B\in V\to \left(B\in \left(A/R\right)\leftrightarrow \exists x\in AB=\left[x\right]R\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢y=B\to \left(y=\left[x\right]R\leftrightarrow B=\left[x\right]R\right)$$
2	1	rexbidv	$$⊢y=B\to \left(\exists x\in Ay=\left[x\right]R\leftrightarrow \exists x\in AB=\left[x\right]R\right)$$
3		df-qs	$$⊢A/R=\left\{y|\exists x\in Ay=\left[x\right]R\right\}$$
4	2 3	elab2g	$$⊢B\in V\to \left(B\in \left(A/R\right)\leftrightarrow \exists x\in AB=\left[x\right]R\right)$$