Theorem qsid

Description: A set is equal to its quotient set modulo the converse membership relation. (Note: the converse membership relation is not an equivalence relation.) (Contributed by NM, 13-Aug-1995) (Revised by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Assertion	qsid	$$⊢A/{\mathrm{E}}^{-1}=A$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	ecid	$$⊢\left[x\right]{\mathrm{E}}^{-1}=x$$
3	2	eqeq2i	$$⊢y=\left[x\right]{\mathrm{E}}^{-1}\leftrightarrow y=x$$
4		equcom	$$⊢y=x\leftrightarrow x=y$$
5	3 4	bitri	$$⊢y=\left[x\right]{\mathrm{E}}^{-1}\leftrightarrow x=y$$
6	5	rexbii	$$⊢\exists x\in Ay=\left[x\right]{\mathrm{E}}^{-1}\leftrightarrow \exists x\in Ax=y$$
7		vex	$$⊢y\in \mathrm{V}$$
8	7	elqs	$$⊢y\in \left(A/{\mathrm{E}}^{-1}\right)\leftrightarrow \exists x\in Ay=\left[x\right]{\mathrm{E}}^{-1}$$
9		risset	$$⊢y\in A\leftrightarrow \exists x\in Ax=y$$
10	6 8 9	3bitr4i	$$⊢y\in \left(A/{\mathrm{E}}^{-1}\right)\leftrightarrow y\in A$$
11	10	eqriv	$$⊢A/{\mathrm{E}}^{-1}=A$$