Theorem elrnressn

Description: Element of the range of a restriction to a singleton. (Contributed by Peter Mazsa, 12-Jun-2024)

	Ref	Expression
Assertion	elrnressn	$$⊢\left(A\in V\wedge B\in W\right)\to \left(B\in \mathrm{ran}\left({R\upharpoonright }_{\left\{A\right\}}\right)\leftrightarrow ARB\right)$$

Proof

Step	Hyp	Ref	Expression
1		elrnres	$$⊢B\in W\to \left(B\in \mathrm{ran}\left({R\upharpoonright }_{\left\{A\right\}}\right)\leftrightarrow \exists x\in \left\{A\right\}xRB\right)$$
2		breq1	$$⊢x=A\to \left(xRB\leftrightarrow ARB\right)$$
3	2	rexsng	$$⊢A\in V\to \left(\exists x\in \left\{A\right\}xRB\leftrightarrow ARB\right)$$
4	1 3	sylan9bbr	$$⊢\left(A\in V\wedge B\in W\right)\to \left(B\in \mathrm{ran}\left({R\upharpoonright }_{\left\{A\right\}}\right)\leftrightarrow ARB\right)$$