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 } )