Theorem rncnvepres

Description: The range of the restricted converse epsilon is the union of the restriction. (Contributed by Peter Mazsa, 11-Feb-2018) (Revised by Peter Mazsa, 26-Sep-2021)

	Ref	Expression
Assertion	rncnvepres	$$⊢\mathrm{ran}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		rnopab	$$⊢\mathrm{ran}\left\{⟨x,y⟩|\left(x\in A\wedge y\in x\right)\right\}=\left\{y|\exists x\left(x\in A\wedge y\in x\right)\right\}$$
2		cnvepres	$$⊢{{\mathrm{E}}^{-1}\upharpoonright }_A=\left\{⟨x,y⟩|\left(x\in A\wedge y\in x\right)\right\}$$
3	2	rneqi	$$⊢\mathrm{ran}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=\mathrm{ran}\left\{⟨x,y⟩|\left(x\in A\wedge y\in x\right)\right\}$$
4		dfuni2	$$⊢\bigcup A=\left\{y|\exists x\in Ay\in x\right\}$$
5		df-rex	$$⊢\exists x\in Ay\in x\leftrightarrow \exists x\left(x\in A\wedge y\in x\right)$$
6	5	abbii	$$⊢\left\{y|\exists x\in Ay\in x\right\}=\left\{y|\exists x\left(x\in A\wedge y\in x\right)\right\}$$
7	4 6	eqtri	$$⊢\bigcup A=\left\{y|\exists x\left(x\in A\wedge y\in x\right)\right\}$$
8	1 3 7	3eqtr4i	$$⊢\mathrm{ran}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=\bigcup A$$