Theorem cnvepres

Description: Restricted converse epsilon relation as a class of ordered pairs. (Contributed by Peter Mazsa, 10-Feb-2018)

	Ref	Expression
Assertion	cnvepres	$$⊢{{\mathrm{E}}^{-1}\upharpoonright }_A=\left\{⟨x,y⟩|\left(x\in A\wedge y\in x\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfres2	$$⊢{{\mathrm{E}}^{-1}\upharpoonright }_A=\left\{⟨x,y⟩|\left(x\in A\wedge x{\mathrm{E}}^{-1}y\right)\right\}$$
2		brcnvep	$$⊢x\in \mathrm{V}\to \left(x{\mathrm{E}}^{-1}y\leftrightarrow y\in x\right)$$
3	2	elv	$$⊢x{\mathrm{E}}^{-1}y\leftrightarrow y\in x$$
4	3	anbi2i	$$⊢\left(x\in A\wedge x{\mathrm{E}}^{-1}y\right)\leftrightarrow \left(x\in A\wedge y\in x\right)$$
5	4	opabbii	$$⊢\left\{⟨x,y⟩|\left(x\in A\wedge x{\mathrm{E}}^{-1}y\right)\right\}=\left\{⟨x,y⟩|\left(x\in A\wedge y\in x\right)\right\}$$
6	1 5	eqtri	$$⊢{{\mathrm{E}}^{-1}\upharpoonright }_A=\left\{⟨x,y⟩|\left(x\in A\wedge y\in x\right)\right\}$$