Theorem eleccnvep

Description: Elementhood in the converse epsilon coset of A is elementhood in A . (Contributed by Peter Mazsa, 27-Jan-2019)

	Ref	Expression
Assertion	eleccnvep	$$⊢A\in V\to \left(B\in \left[A\right]{\mathrm{E}}^{-1}\leftrightarrow B\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{\mathrm{E}}^{-1}$$
2		relelec	$$⊢\mathrm{Rel}{\mathrm{E}}^{-1}\to \left(B\in \left[A\right]{\mathrm{E}}^{-1}\leftrightarrow A{\mathrm{E}}^{-1}B\right)$$
3	1 2	ax-mp	$$⊢B\in \left[A\right]{\mathrm{E}}^{-1}\leftrightarrow A{\mathrm{E}}^{-1}B$$
4		brcnvep	$$⊢A\in V\to \left(A{\mathrm{E}}^{-1}B\leftrightarrow B\in A\right)$$
5	3 4	bitrid	$$⊢A\in V\to \left(B\in \left[A\right]{\mathrm{E}}^{-1}\leftrightarrow B\in A\right)$$