Theorem elqsecl

Description: Membership in a quotient set by an equivalence class according to .~ . (Contributed by Alexander van der Vekens, 12-Apr-2018) (Revised by AV, 30-Apr-2021)

	Ref	Expression
Assertion	elqsecl	$$⊢B\in X\to \left(B\in \left(W/\underset{\dot{}}{\sim }\right)\leftrightarrow \exists x\in WB=\left\{y|x\underset{\dot{}}{\sim }y\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		elqsg	$$⊢B\in X\to \left(B\in \left(W/\underset{\dot{}}{\sim }\right)\leftrightarrow \exists x\in WB=\left[x\right]\underset{\dot{}}{\sim }\right)$$
2		vex	$$⊢x\in \mathrm{V}$$
3		dfec2	$$⊢x\in \mathrm{V}\to \left[x\right]\underset{\dot{}}{\sim }=\left\{y|x\underset{\dot{}}{\sim }y\right\}$$
4	2 3	mp1i	$$⊢B\in X\to \left[x\right]\underset{\dot{}}{\sim }=\left\{y|x\underset{\dot{}}{\sim }y\right\}$$
5	4	eqeq2d	$$⊢B\in X\to \left(B=\left[x\right]\underset{\dot{}}{\sim }\leftrightarrow B=\left\{y|x\underset{\dot{}}{\sim }y\right\}\right)$$
6	5	rexbidv	$$⊢B\in X\to \left(\exists x\in WB=\left[x\right]\underset{\dot{}}{\sim }\leftrightarrow \exists x\in WB=\left\{y|x\underset{\dot{}}{\sim }y\right\}\right)$$
7	1 6	bitrd	$$⊢B\in X\to \left(B\in \left(W/\underset{\dot{}}{\sim }\right)\leftrightarrow \exists x\in WB=\left\{y|x\underset{\dot{}}{\sim }y\right\}\right)$$