Theorem eccnvepres

Description: Restricted converse epsilon coset of B . (Contributed by Peter Mazsa, 11-Feb-2018) (Revised by Peter Mazsa, 21-Oct-2021)

	Ref	Expression
Assertion	eccnvepres	$$⊢B\in V\to \left[B\right]\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=\left\{x\in B|B\in A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		brcnvep	$$⊢B\in V\to \left(B{\mathrm{E}}^{-1}x\leftrightarrow x\in B\right)$$
2	1	anbi1cd	$$⊢B\in V\to \left(\left(B\in A\wedge B{\mathrm{E}}^{-1}x\right)\leftrightarrow \left(x\in B\wedge B\in A\right)\right)$$
3	2	abbidv	$$⊢B\in V\to \left\{x|\left(B\in A\wedge B{\mathrm{E}}^{-1}x\right)\right\}=\left\{x|\left(x\in B\wedge B\in A\right)\right\}$$
4		ecres	$$⊢\left[B\right]\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=\left\{x|\left(B\in A\wedge B{\mathrm{E}}^{-1}x\right)\right\}$$
5		df-rab	$$⊢\left\{x\in B|B\in A\right\}=\left\{x|\left(x\in B\wedge B\in A\right)\right\}$$
6	3 4 5	3eqtr4g	$$⊢B\in V\to \left[B\right]\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=\left\{x\in B|B\in A\right\}$$