Theorem cnvepresex

Description: Sethood condition for the restricted converse epsilon relation. (Contributed by Peter Mazsa, 24-Sep-2018)

	Ref	Expression
Assertion	cnvepresex	$$⊢A\in V\to {{\mathrm{E}}^{-1}\upharpoonright }_A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		cnvepres	$$⊢{{\mathrm{E}}^{-1}\upharpoonright }_A=\left\{⟨x,y⟩|\left(x\in A\wedge y\in x\right)\right\}$$
2		id	$$⊢A\in V\to A\in V$$
3		abid2	$$⊢\left\{y|y\in x\right\}=x$$
4		vex	$$⊢x\in \mathrm{V}$$
5	3 4	eqeltri	$$⊢\left\{y|y\in x\right\}\in \mathrm{V}$$
6	5	a1i	$$⊢\left(A\in V\wedge x\in A\right)\to \left\{y|y\in x\right\}\in \mathrm{V}$$
7	2 6	opabex3d	$$⊢A\in V\to \left\{⟨x,y⟩|\left(x\in A\wedge y\in x\right)\right\}\in \mathrm{V}$$
8	1 7	eqeltrid	$$⊢A\in V\to {{\mathrm{E}}^{-1}\upharpoonright }_A\in \mathrm{V}$$