Theorem brcnvep

Description: The converse of the binary epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018)

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

Proof

Step	Hyp	Ref	Expression
1		rele	$$⊢\mathrm{Rel}\mathrm{E}$$
2	1	relbrcnv	$$⊢A{\mathrm{E}}^{-1}B\leftrightarrow B\mathrm{E}A$$
3		epelg	$$⊢A\in V\to \left(B\mathrm{E}A\leftrightarrow B\in A\right)$$
4	2 3	bitrid	$$⊢A\in V\to \left(A{\mathrm{E}}^{-1}B\leftrightarrow B\in A\right)$$