Theorem rnxrnidres

Description: Range of a range Cartesian product with a restriction of the identity relation. (Contributed by Peter Mazsa, 6-Dec-2021)

	Ref	Expression
Assertion	rnxrnidres	$$⊢\mathrm{ran}R⋉\left({\mathrm{I}\upharpoonright }_A\right)=\left\{⟨x,y⟩|\exists u\in A\left(u=y\wedge uRx\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		rnxrnres	$$⊢\mathrm{ran}R⋉\left({\mathrm{I}\upharpoonright }_A\right)=\left\{⟨x,y⟩|\exists u\in A\left(uRx\wedge u\mathrm{I}y\right)\right\}$$
2		ideqg	$$⊢y\in \mathrm{V}\to \left(u\mathrm{I}y\leftrightarrow u=y\right)$$
3	2	elv	$$⊢u\mathrm{I}y\leftrightarrow u=y$$
4	3	anbi1ci	$$⊢\left(uRx\wedge u\mathrm{I}y\right)\leftrightarrow \left(u=y\wedge uRx\right)$$
5	4	rexbii	$$⊢\exists u\in A\left(uRx\wedge u\mathrm{I}y\right)\leftrightarrow \exists u\in A\left(u=y\wedge uRx\right)$$
6	5	opabbii	$$⊢\left\{⟨x,y⟩|\exists u\in A\left(uRx\wedge u\mathrm{I}y\right)\right\}=\left\{⟨x,y⟩|\exists u\in A\left(u=y\wedge uRx\right)\right\}$$
7	1 6	eqtri	$$⊢\mathrm{ran}R⋉\left({\mathrm{I}\upharpoonright }_A\right)=\left\{⟨x,y⟩|\exists u\in A\left(u=y\wedge uRx\right)\right\}$$