This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 x ) -> A e. _V )
8 7 stoic1a 
 |-  ( ( Rel R /\ -. A e. _V ) -> -. A R x )
9 8 alrimiv 
 |-  ( ( Rel R /\ -. A e. _V ) -> A. x -. A R x )
10 breq2 
 |-  ( y = x -> ( A R y <-> A R x ) )
11 10 ab0w 
 |-  ( { y | A R y } = (/) <-> A. x -. A R x )
12 9 11 sylibr 
 |-  ( ( 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 } )