Theorem imasng

Description: The image of a singleton. (Contributed by NM, 8-May-2005)

	Ref	Expression
Assertion	imasng	$$⊢A\in B\to R\left[\left\{A\right\}\right]=\left\{y|ARy\right\}$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in B\to A\in \mathrm{V}$$
2		dfima2	$$⊢R\left[\left\{A\right\}\right]=\left\{y|\exists x\in \left\{A\right\}xRy\right\}$$
3		breq1	$$⊢x=A\to \left(xRy\leftrightarrow ARy\right)$$
4	3	rexsng	$$⊢A\in \mathrm{V}\to \left(\exists x\in \left\{A\right\}xRy\leftrightarrow ARy\right)$$
5	4	abbidv	$$⊢A\in \mathrm{V}\to \left\{y|\exists x\in \left\{A\right\}xRy\right\}=\left\{y|ARy\right\}$$
6	2 5	eqtrid	$$⊢A\in \mathrm{V}\to R\left[\left\{A\right\}\right]=\left\{y|ARy\right\}$$
7	1 6	syl	$$⊢A\in B\to R\left[\left\{A\right\}\right]=\left\{y|ARy\right\}$$