Metamath Proof Explorer


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 eqtrdi
 |-  ( -. 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 } )