Theorem imasng

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

	Ref	Expression
Assertion	imasng	|- ( A e. B -> ( R " { A } ) = { y | A R y } )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( A e. B -> A e. _V )
2		dfima2	|- ( R " { A } ) = { y | E. x e. { A } x R y }
3		breq1	|- ( x = A -> ( x R y <-> A R y ) )
4	3	rexsng	|- ( A e. _V -> ( E. x e. { A } x R y <-> A R y ) )
5	4	abbidv	|- ( A e. _V -> { y | E. x e. { A } x R y } = { y | A R y } )
6	2 5	eqtrid	|- ( A e. _V -> ( R " { A } ) = { y | A R y } )
7	1 6	syl	|- ( A e. B -> ( R " { A } ) = { y | A R y } )