Theorem ecid

Description: A set is equal to its coset under 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
Hypothesis	ecid.1	$$⊢A\in \mathrm{V}$$
Assertion	ecid	$$⊢\left[A\right]{\mathrm{E}}^{-1}=A$$

Proof

Step	Hyp	Ref	Expression
1		ecid.1	$$⊢A\in \mathrm{V}$$
2		vex	$$⊢y\in \mathrm{V}$$
3	2 1	elec	$$⊢y\in \left[A\right]{\mathrm{E}}^{-1}\leftrightarrow A{\mathrm{E}}^{-1}y$$
4	1 2	brcnv	$$⊢A{\mathrm{E}}^{-1}y\leftrightarrow y\mathrm{E}A$$
5	1	epeli	$$⊢y\mathrm{E}A\leftrightarrow y\in A$$
6	3 4 5	3bitri	$$⊢y\in \left[A\right]{\mathrm{E}}^{-1}\leftrightarrow y\in A$$
7	6	eqriv	$$⊢\left[A\right]{\mathrm{E}}^{-1}=A$$