Theorem relimasn

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

	Ref	Expression
Assertion	relimasn	|- ( Rel R -> ( R " { A } ) = { y | A R y } )

Proof

Step	Hyp	Ref	Expression
1		snprc	|- ( -. A e. _V <-> { A } = (/) )
2		imaeq2	|- ( { A } = (/) -> ( R " { A } ) = ( R " (/) ) )
3	1 2	sylbi	|- ( -. A e. _V -> ( R " { A } ) = ( R " (/) ) )
4		ima0	|- ( R " (/) ) = (/)
5	3 4	syl6eq	|- ( -. A e. _V -> ( R " { A } ) = (/) )
6	5	adantl	|- ( ( Rel R /\ -. A e. _V ) -> ( R " { A } ) = (/) )
7		brrelex1	|- ( ( Rel R /\ A R y ) -> A e. _V )
8	7	stoic1a	|- ( ( Rel R /\ -. A e. _V ) -> -. A R y )
9	8	nexdv	|- ( ( Rel R /\ -. A e. _V ) -> -. E. y A R y )
10		abn0	|- ( { y | A R y } =/= (/) <-> E. y A R y )
11	10	necon1bbii	|- ( -. E. y A R y <-> { y | A R y } = (/) )
12	9 11	sylib	|- ( ( Rel R /\ -. A e. _V ) -> { y | A R y } = (/) )
13	6 12	eqtr4d	|- ( ( Rel R /\ -. A e. _V ) -> ( R " { A } ) = { y | A R y } )
14	13	ex	|- ( Rel R -> ( -. A e. _V -> ( R " { A } ) = { y | A R y } ) )
15		imasng	|- ( A e. _V -> ( R " { A } ) = { y | A R y } )
16	14 15	pm2.61d2	|- ( Rel R -> ( R " { A } ) = { y | A R y } )